Lecture III (§3) — the function space (𝒟₀ → 𝒟₁): Definitions 3.8, Propositions

3.9, Theorems 3.10, 3.11, 3.12, 3.13

Following Dana Scott, Lectures on a Mathematical Theory of Computation, PRG-19 (1981), Lecture III. The function space (𝒟₀ → 𝒟₁) is the neighbourhood system whose tokens are the approximable maps 𝒟₀ → 𝒟₁ (Definition 2.1), and whose neighbourhoods are the non-empty finite intersections of the step sets

[X, Y] = {f ∣ X f Y} (step X Y),

for X ∈ 𝒟₀, Y ∈ 𝒟₁. We model a finite intersection by a List of (X, Y) pairs, with stepFun L = {f ∣ ∀ (X, Y) ∈ L, X f Y}; the empty list gives the master Δ = |𝒟₀ → 𝒟₁| (Set.univ). The system is positive: a neighbourhood is required non-empty, which is exactly what makes a filter's induced relation intersective (Theorem 3.10).

This file formalizes:

• Definition 3.8 — step, stepFun, the system funSpace V₀ V₁, with the basic algebra step_inter_right ([X,Y] ∩ [X,Y'] = [X,Y∩Y']), step_subset (antitone/monotone), step_master_eq ([Δ₀,Δ₁] = univ), and membership step_mem.
• Theorem 3.10 (the crux) — funSpaceEquiv : |𝒟₀ → 𝒟₁| ≃o ApproximableMap V₀ V₁: every filter is fixed by a unique approximable map (toApproxMap/toFilter), inclusion-preservingly.
• Proposition 3.9 — leastMap (the least map f₀ of a consistent neighbourhood, condition (ii) X f₀ Y ↔ ⋂{Yᵢ ∣ X ⊆ Xᵢ} ⊆ Y), leastMap_mem_stepFun and leastMap_le (it is the minimal element of ⋂[Xᵢ,Yᵢ]), and stepFun_subset_step_iff (the remark after 3.9). The consistency hypothesis hcons is Scott's condition (i) in operational form.
• Theorem 3.13 — le_iff_toElementMap_le (i); mapsBounded_iff_pointwiseBounded (ii); sSupMaps with toElementMap_sSupMaps (iii).

The order on approximable maps (rel-inclusion).

@[implicit_reducible]

instance Domain.Neighborhood.instPartialOrderApproximableMap {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} : PartialOrder (ApproximableMap V₀ V₁)

Approximable maps are ordered by inclusion of their relations (Scott's approximation order on |𝒟₀ → 𝒟₁|). Antisymmetry is ApproximableMap.ext.

Equations

• One or more equations did not get rendered due to their size.

theorem Domain.Neighborhood.ApproximableMap.le_iff {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {f g : ApproximableMap V₀ V₁} : f ≤ g ↔ ∀ (X : Set α) (Y : Set β), f.rel X Y → g.rel X Y

Definition 3.8 — step sets and the function space.

def Domain.Neighborhood.step {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (X : Set α) (Y : Set β) : Set (ApproximableMap V₀ V₁)

Scott's step set [X, Y] = {f ∣ X f Y}.

Equations

• Domain.Neighborhood.step X Y = {f : Domain.Neighborhood.ApproximableMap V₀ V₁ | f.rel X Y}

@[simp]

theorem Domain.Neighborhood.mem_step {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {X : Set α} {Y : Set β} {f : ApproximableMap V₀ V₁} : f ∈ step X Y ↔ f.rel X Y

def Domain.Neighborhood.stepFun {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (L : List (Set α × Set β)) : Set (ApproximableMap V₀ V₁)

A finite intersection of step sets, indexed by a list of (X, Y) pairs.

Equations

• Domain.Neighborhood.stepFun L = {f : Domain.Neighborhood.ApproximableMap V₀ V₁ | ∀ p ∈ L, f.rel p.1 p.2}

@[simp]

theorem Domain.Neighborhood.mem_stepFun {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {L : List (Set α × Set β)} {f : ApproximableMap V₀ V₁} : f ∈ stepFun L ↔ ∀ p ∈ L, f.rel p.1 p.2

@[simp]

theorem Domain.Neighborhood.stepFun_nil {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} : stepFun [] = Set.univ

theorem Domain.Neighborhood.stepFun_cons {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (p : Set α × Set β) (L : List (Set α × Set β)) : stepFun (p :: L) = step p.1 p.2 ∩ stepFun L

theorem Domain.Neighborhood.stepFun_append {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (L L' : List (Set α × Set β)) : stepFun (L ++ L') = stepFun L ∩ stepFun L'

theorem Domain.Neighborhood.stepFun_singleton {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (X : Set α) (Y : Set β) : stepFun [(X, Y)] = step X Y

@[simp]

theorem Domain.Neighborhood.step_master_eq {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} : step V₀.master V₁.master = Set.univ

[Δ₀, Δ₁] = |𝒟₀ → 𝒟₁|: every map relates the masters.

theorem Domain.Neighborhood.step_inter_right {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {X : Set α} {Y Y' : Set β} (hY : V₁.mem Y) (hY' : V₁.mem Y') : step X Y ∩ step X Y' = step X (Y ∩ Y')

[X, Y] ∩ [X, Y'] = [X, Y ∩ Y'] (intersectivity in the output).

theorem Domain.Neighborhood.step_subset {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {X X' : Set α} {Y Y' : Set β} (hX' : V₀.mem X') (hY' : V₁.mem Y') (hX'X : X' ⊆ X) (hYY' : Y ⊆ Y') : step X Y ⊆ step X' Y'

X' ⊆ X and Y ⊆ Y' imply [X, Y] ⊆ [X', Y'].

def Domain.Neighborhood.funSpace {α : Type u_1} {β : Type u_2} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) : NeighborhoodSystem (ApproximableMap V₀ V₁)

Definition 3.8 (Scott 1981, PRG-19). The function space (𝒟₀ → 𝒟₁): tokens are approximable maps, neighbourhoods are non-empty finite intersections of step sets.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Domain.Neighborhood.funSpace_master {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} : (funSpace V₀ V₁).master = Set.univ

theorem Domain.Neighborhood.funSpace_mem_iff {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {W : Set (ApproximableMap V₀ V₁)} : (funSpace V₀ V₁).mem W ↔ (∃ (L : List (Set α × Set β)), (∀ p ∈ L, V₀.mem p.1 ∧ V₁.mem p.2) ∧ W = stepFun L) ∧ W.Nonempty

theorem Domain.Neighborhood.step_mem {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {X : Set α} {Y : Set β} (hX : V₀.mem X) (hY : V₁.mem Y) : (funSpace V₀ V₁).mem (step X Y)

A step neighbourhood [X, Y] is a neighbourhood of the function space (non-empty: it contains the constant map constMap V₀ (↑Y)).

theorem Domain.Neighborhood.mem_stepFun_iff {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (φ : (funSpace V₀ V₁).Element) {L : List (Set α × Set β)} (hL : ∀ p ∈ L, V₀.mem p.1 ∧ V₁.mem p.2) : φ.mem (stepFun L) ↔ ∀ p ∈ L, φ.mem (step p.1 p.2)

The "generation" lemma: a filter contains the intersection stepFun L iff it contains each step [Xᵢ, Yᵢ]. (The step sets [X, Y] ∈ φ generate the filter φ.)

Theorem 3.10 — the function space is complete.

def Domain.Neighborhood.toApproxMap {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (φ : (funSpace V₀ V₁).Element) : ApproximableMap V₀ V₁

Theorem 3.10 (Scott 1981, PRG-19). The relation X φ̂ Y ↔ [X, Y] ∈ φ of a filter φ. Intersectivity is the payoff of positivity ([X,Y]∩[X,Y'] = [X,Y∩Y'] is non-empty, so Y∩Y' ∈ 𝒟₁).

Equations

• Domain.Neighborhood.toApproxMap φ = { rel := fun (X : Set α) (Y : Set β) => φ.mem (Domain.Neighborhood.step X Y), rel_dom := ⋯, rel_cod := ⋯, master_rel := ⋯, inter_right := ⋯, mono := ⋯ }

@[simp]

theorem Domain.Neighborhood.toApproxMap_rel {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {φ : (funSpace V₀ V₁).Element} {X : Set α} {Y : Set β} : (toApproxMap φ).rel X Y ↔ φ.mem (step X Y)

def Domain.Neighborhood.toFilter {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (f : ApproximableMap V₀ V₁) : (funSpace V₀ V₁).Element

Theorem 3.10 (Scott 1981, PRG-19). The filter f̂ = {F ∣ f ∈ F} of an approximable map.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Domain.Neighborhood.mem_toFilter {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {f : ApproximableMap V₀ V₁} {W : Set (ApproximableMap V₀ V₁)} : (toFilter f).mem W ↔ (funSpace V₀ V₁).mem W ∧ f ∈ W

def Domain.Neighborhood.funSpaceEquiv {α : Type u_1} {β : Type u_2} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) : (funSpace V₀ V₁).Element ≃o ApproximableMap V₀ V₁

Theorem 3.10 (Scott 1981, PRG-19). The function space is complete: every filter is fixed by a unique approximable mapping, inclusion-preservingly.

Equations

• Domain.Neighborhood.funSpaceEquiv V₀ V₁ = { toFun := Domain.Neighborhood.toApproxMap, invFun := Domain.Neighborhood.toFilter, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem Domain.Neighborhood.funSpaceEquiv_apply {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (φ : (funSpace V₀ V₁).Element) : (funSpaceEquiv V₀ V₁) φ = toApproxMap φ

@[simp]

theorem Domain.Neighborhood.funSpaceEquiv_symm_apply {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (f : ApproximableMap V₀ V₁) : (funSpaceEquiv V₀ V₁).symm f = toFilter f

theorem Domain.Neighborhood.funSpace_mem_inter {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {W W' : Set (ApproximableMap V₀ V₁)} (hW : (funSpace V₀ V₁).mem W) (hW' : (funSpace V₀ V₁).mem W') (hne : (W ∩ W').Nonempty) : (funSpace V₀ V₁).mem (W ∩ W')

Intersection of two function-space neighbourhoods, when non-empty, is again one.

theorem Domain.Neighborhood.stepFun_up_closed {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {L : List (Set α × Set β)} {f f' : ApproximableMap V₀ V₁} (hf : f ∈ stepFun L) (hff' : f ≤ f') : f' ∈ stepFun L

Step neighbourhoods are up-closed under the map order: if f ∈ stepFun L and f ⊑ f', then f' ∈ stepFun L.

theorem Domain.Neighborhood.funSpace_mem_up_closed {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {W : Set (ApproximableMap V₀ V₁)} (hW : (funSpace V₀ V₁).mem W) {f f' : ApproximableMap V₀ V₁} (hf : f ∈ W) (hff' : f ≤ f') : f' ∈ W

A function-space neighbourhood is up-closed under the map order.

Proposition 3.9 — the least map of a consistent neighbourhood.

def Domain.Neighborhood.interYs {α : Type u_1} {β : Type u_2} (m : Set β) : List (Set α × Set β) → Set α → Set β

Scott's intersection ⋂ {Yᵢ ∣ X ⊆ Xᵢ} of the outputs whose input is coarser than X, taken inside the master neighbourhood Δ₁ (so the empty intersection is Δ₁, per the convention 1.1a). Indexed by the list L of (Xᵢ, Yᵢ) pairs.

Equations

• Domain.Neighborhood.interYs m [] x✝ = m
• Domain.Neighborhood.interYs m (p :: L) x✝ = {z : β | x✝ ⊆ p.1 → z ∈ p.2} ∩ Domain.Neighborhood.interYs m L x✝

@[simp]

theorem Domain.Neighborhood.interYs_nil {α : Type u_1} {β : Type u_2} (m : Set β) (X : Set α) : interYs m [] X = m

theorem Domain.Neighborhood.interYs_cons {α : Type u_1} {β : Type u_2} (m : Set β) (p : Set α × Set β) (L : List (Set α × Set β)) (X : Set α) : interYs m (p :: L) X = {z : β | X ⊆ p.1 → z ∈ p.2} ∩ interYs m L X

theorem Domain.Neighborhood.mem_interYs {α : Type u_1} {β : Type u_2} {m : Set β} {L : List (Set α × Set β)} {X : Set α} {z : β} : z ∈ interYs m L X ↔ z ∈ m ∧ ∀ p ∈ L, X ⊆ p.1 → z ∈ p.2

Membership in interYs: z ∈ ⋂{Yᵢ ∣ X ⊆ Xᵢ} iff z ∈ Δ₁ and z ∈ Yᵢ for every i with X ⊆ Xᵢ.

theorem Domain.Neighborhood.interYs_subset_master {α : Type u_1} {β : Type u_2} {m : Set β} {L : List (Set α × Set β)} {X : Set α} : interYs m L X ⊆ m

interYs is contained in the master neighbourhood.

theorem Domain.Neighborhood.interYs_antitone {α : Type u_1} {β : Type u_2} {m : Set β} {L : List (Set α × Set β)} {X X' : Set α} (h : X' ⊆ X) : interYs m L X' ⊆ interYs m L X

interYs is antitone in the input X: a sharper input intersects over more outputs.

theorem Domain.Neighborhood.interYs_subset_of_mem {α : Type u_1} {β : Type u_2} {m : Set β} {L : List (Set α × Set β)} {p : Set α × Set β} (hp : p ∈ L) : interYs m L p.1 ⊆ p.2

interYs contains Yⱼ whenever Xⱼ ⊆ X-indexed: in particular interYs m L Xⱼ ⊆ Yⱼ for (Xⱼ, Yⱼ) ∈ L.

def Domain.Neighborhood.leastMap {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (L : List (Set α × Set β)) (hcons : ∀ {X : Set α}, V₀.mem X → V₁.mem (interYs V₁.master L X)) : ApproximableMap V₀ V₁

Proposition 3.9(ii) (Scott 1981, PRG-19). The least approximable mapping f₀ belonging to the neighbourhood ⋂ [Xᵢ, Yᵢ], defined by X f₀ Y ↔ ⋂{Yᵢ ∣ X ⊆ Xᵢ} ⊆ Y. Well-definedness uses Scott's condition (i) in the operational form hcons: for every neighbourhood X, the outputs {Yᵢ ∣ X ⊆ Xᵢ} (consistent in 𝒟₁, witnessed by X being a common lower bound of their inputs) have their intersection again a neighbourhood.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Domain.Neighborhood.leastMap_rel {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {L : List (Set α × Set β)} {hcons : ∀ {X : Set α}, V₀.mem X → V₁.mem (interYs V₁.master L X)} {X : Set α} {Y : Set β} : (leastMap L ⋯).rel X Y ↔ V₀.mem X ∧ V₁.mem Y ∧ interYs V₁.master L X ⊆ Y

theorem Domain.Neighborhood.leastMap_mem_stepFun {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {L : List (Set α × Set β)} (hL : ∀ p ∈ L, V₀.mem p.1 ∧ V₁.mem p.2) (hcons : ∀ {X : Set α}, V₀.mem X → V₁.mem (interYs V₁.master L X)) : leastMap L ⋯ ∈ stepFun L

Proposition 3.9 (Scott 1981, PRG-19). The least map f₀ belongs to the neighbourhood: Xᵢ f₀ Yᵢ for every (Xᵢ, Yᵢ) ∈ L.

theorem Domain.Neighborhood.rel_interYs {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {L : List (Set α × Set β)} {f : ApproximableMap V₀ V₁} (hf : f ∈ stepFun L) {X : Set α} (hX : V₀.mem X) : f.rel X (interYs V₁.master L X)

The relation X f Y holds for f in the neighbourhood stepFun L at the master output, and more importantly f relates X to the whole intersection interYs Δ₁ L X (finite intersectivity over the relevant outputs). The case split deciding X ⊆ Xᵢ is a documented classical step.

theorem Domain.Neighborhood.leastMap_le {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {L : List (Set α × Set β)} (hcons : ∀ {X : Set α}, V₀.mem X → V₁.mem (interYs V₁.master L X)) {f : ApproximableMap V₀ V₁} (hf : f ∈ stepFun L) : leastMap L ⋯ ≤ f

Proposition 3.9 (Scott 1981, PRG-19). f₀ is the minimal element of the neighbourhood: any f with Xᵢ f Yᵢ for all i satisfies f₀ ⊆ f.

theorem Domain.Neighborhood.stepFun_subset_step_iff {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {L : List (Set α × Set β)} (hL : ∀ p ∈ L, V₀.mem p.1 ∧ V₁.mem p.2) (hcons : ∀ {X : Set α}, V₀.mem X → V₁.mem (interYs V₁.master L X)) {X : Set α} {Y : Set β} (hX : V₀.mem X) (hY : V₁.mem Y) : stepFun L ⊆ step X Y ↔ interYs V₁.master L X ⊆ Y

Remark after Proposition 3.9 (Scott 1981, PRG-19). When the neighbourhood is consistent, ⋂ [Xᵢ, Yᵢ] ⊆ [X, Y] iff ⋂{Yᵢ ∣ X ⊆ Xᵢ} ⊆ Y. This is the form used to check that curry is monotone (and hence approximable).

Theorem 3.13(i) — the pointwise order.

theorem Domain.Neighborhood.le_iff_toElementMap_le {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {f g : ApproximableMap V₀ V₁} : f ≤ g ↔ ∀ (x : V₀.Element), f.toElementMap x ≤ g.toElementMap x

Theorem 3.13(i) (Scott 1981, PRG-19). f ⊑ g ↔ ∀ x, f(x) ⊑ g(x).

Theorem 3.13(ii)(iii) — pointwise boundedness and sups.

def Domain.Neighborhood.MapsBounded {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (F : Set (ApproximableMap V₀ V₁)) : Prop

A set F of approximable maps is bounded when it has an upper bound in the map order.

Equations

• Domain.Neighborhood.MapsBounded F = ∃ (h : Domain.Neighborhood.ApproximableMap V₀ V₁), ∀ f ∈ F, f ≤ h

def Domain.Neighborhood.PointwiseBounded {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (F : Set (ApproximableMap V₀ V₁)) : Prop

F is pointwise bounded when {f(x) ∣ f ∈ F} is bounded in |𝒟₁| for every x.

Equations

• Domain.Neighborhood.PointwiseBounded F = ∀ (x : V₀.Element), V₁.Bounded ((fun (f : Domain.Neighborhood.ApproximableMap V₀ V₁) => f.toElementMap x) '' F)

theorem Domain.Neighborhood.toFilter_le_iff {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {f g : ApproximableMap V₀ V₁} : toFilter f ≤ toFilter g ↔ f ≤ g

theorem Domain.Neighborhood.mapsBounded_principal {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {F : Set (ApproximableMap V₀ V₁)} (hF : PointwiseBounded F) {X : Set α} (hX : V₀.mem X) : V₁.Bounded ((fun (f : ApproximableMap V₀ V₁) => f.toElementMap (V₀.principal hX)) '' F)

def Domain.Neighborhood.supOnPrincipal {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (F : Set (ApproximableMap V₀ V₁)) (hF : PointwiseBounded F) (X : Set α) (hX : V₀.mem X) : V₁.Element

The sup of {f(↑X) ∣ f ∈ F} on principal inputs, used to build sSupMaps.

Equations

• Domain.Neighborhood.supOnPrincipal F hF X hX = V₁.sSup ((fun (f : Domain.Neighborhood.ApproximableMap V₀ V₁) => f.toElementMap (V₀.principal hX)) '' F) ⋯

theorem Domain.Neighborhood.supOnPrincipal_mono {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (F : Set (ApproximableMap V₀ V₁)) (hF : PointwiseBounded F) (X X' : Set α) (hX : V₀.mem X) (hX' : V₀.mem X') (hX'X : X' ⊆ X) : supOnPrincipal F hF X hX ≤ supOnPrincipal F hF X' hX'

theorem Domain.Neighborhood.mapsBounded_to_filters {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {F : Set (ApproximableMap V₀ V₁)} (h : MapsBounded F) : (funSpace V₀ V₁).Bounded (toFilter '' F)

def Domain.Neighborhood.sSupMaps {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (F : Set (ApproximableMap V₀ V₁)) (hF : PointwiseBounded F) : ApproximableMap V₀ V₁

Theorem 3.13(iii) (Scott 1981, PRG-19). The least upper bound of a pointwise-bounded set F, defined on principal inputs by supOnPrincipal and extended via Exercise 2.8 (ofMono).

Equations

• Domain.Neighborhood.sSupMaps F hF = Domain.Neighborhood.ApproximableMap.ofMono (fun (X : Set α) (hX : V₀.mem X) => Domain.Neighborhood.supOnPrincipal F hF X hX) ⋯

theorem Domain.Neighborhood.toElementMap_sSupMaps_principal {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {F : Set (ApproximableMap V₀ V₁)} (hF : PointwiseBounded F) {X : Set α} (hX : V₀.mem X) : (sSupMaps F hF).toElementMap (V₀.principal hX) = supOnPrincipal F hF X hX

theorem Domain.Neighborhood.mapsBounded_iff_pointwiseBounded {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {F : Set (ApproximableMap V₀ V₁)} : MapsBounded F ↔ PointwiseBounded F

Theorem 3.13(ii) (Scott 1981, PRG-19). F is bounded in |𝒟₀ → 𝒟₁| iff {f(x) ∣ f ∈ F} is bounded in |𝒟₁| for each x ∈ |𝒟₀|. The forward direction is le_iff_toElementMap_le (3.13(i)) applied pointwise; the backward direction builds the bound sSupMaps F.

theorem Domain.Neighborhood.le_sSupMaps {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {F : Set (ApproximableMap V₀ V₁)} (hF : PointwiseBounded F) {f : ApproximableMap V₀ V₁} (hf : f ∈ F) : f ≤ sSupMaps F hF

theorem Domain.Neighborhood.sSupMaps_le {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {F : Set (ApproximableMap V₀ V₁)} (hF : PointwiseBounded F) {h : ApproximableMap V₀ V₁} (hh : ∀ f ∈ F, f ≤ h) : sSupMaps F hF ≤ h

theorem Domain.Neighborhood.toElementMap_sSupMaps {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {F : Set (ApproximableMap V₀ V₁)} (hF : PointwiseBounded F) (x : V₀.Element) : (sSupMaps F hF).toElementMap x = V₁.sSup ((fun (f : ApproximableMap V₀ V₁) => f.toElementMap x) '' F) ⋯

theorem Domain.Neighborhood.toElementMap_sSupMaps' {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {F : Set (ApproximableMap V₀ V₁)} (hF : MapsBounded F) (x : V₀.Element) : (sSupMaps F ⋯).toElementMap x = V₁.sSup ((fun (f : ApproximableMap V₀ V₁) => f.toElementMap x) '' F) ⋯

Theorem 3.13(iii) (Scott 1981, PRG-19). When F is bounded, (⊔F)(x) = ⊔{f(x) ∣ f ∈ F} (stated with the boundedness hypothesis in Scott's MapsBounded form).

Theorem 3.11 — evaluation.

def Domain.Neighborhood.eval {β : Type u_2} {γ : Type u_3} (V₁ : NeighborhoodSystem β) (V₂ : NeighborhoodSystem γ) : ApproximableMap₂ (funSpace V₁ V₂) V₁ V₂

Theorem 3.11 (Scott 1981, PRG-19). The two-variable evaluation map eval : (𝒟₁ → 𝒟₂) × 𝒟₁ → 𝒟₂, F, X eval Y ↔ X f Y for all f ∈ F.

Equations

• One or more equations did not get rendered due to their size.

theorem Domain.Neighborhood.toElementMap₂_eval {β : Type u_2} {γ : Type u_3} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} (φ : (funSpace V₁ V₂).Element) (x : V₁.Element) : (eval V₁ V₂).toElementMap₂ φ x = (toApproxMap φ).toElementMap x

Theorem 3.11(i) (Scott 1981, PRG-19). eval(f, x) = f(x) (with the filter φ viewed as the map toApproxMap φ via Theorem 3.10).

def Domain.Neighborhood.evalMap {β : Type u_2} {γ : Type u_3} (V₁ : NeighborhoodSystem β) (V₂ : NeighborhoodSystem γ) : ApproximableMap (prod (funSpace V₁ V₂) V₁) V₂

Theorem 3.11 (Scott 1981, PRG-19). Evaluation as a single approximable map out of the product (𝒟₁ → 𝒟₂) × 𝒟₁ → 𝒟₂.

Equations

• Domain.Neighborhood.evalMap V₁ V₂ = Domain.Neighborhood.ofMap₂ (Domain.Neighborhood.eval V₁ V₂)

theorem Domain.Neighborhood.evalMap_apply {β : Type u_2} {γ : Type u_3} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} (φ : (funSpace V₁ V₂).Element) (x : V₁.Element) : (evalMap V₁ V₂).toElementMap (pair φ x) = (toApproxMap φ).toElementMap x

Theorem 3.11(i) (Scott 1981, PRG-19). eval(⟨f, x⟩) = f(x).

Theorem 3.12 — currying.

def Domain.Neighborhood.gSection {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} (g : ApproximableMap (prod V₀ V₁) V₂) {X : Set α} (hX : V₀.mem X) : ApproximableMap V₁ V₂

The X-section of a two-variable map g : 𝒟₀ × 𝒟₁ → 𝒟₂: the map 𝒟₁ → 𝒟₂ with Y (gSection g X) Z ↔ X ∪ Y g Z.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Domain.Neighborhood.gSection_rel {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {g : ApproximableMap (prod V₀ V₁) V₂} {X : Set α} (hX : V₀.mem X) {Y : Set β} {Z : Set γ} : (gSection g hX).rel Y Z ↔ g.rel (prodNbhd X Y) Z

theorem Domain.Neighborhood.gSection_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {g : ApproximableMap (prod V₀ V₁) V₂} {X X' : Set α} (hX : V₀.mem X) (hX' : V₀.mem X') (hX'X : X' ⊆ X) : gSection g hX ≤ gSection g hX'

def Domain.Neighborhood.curry {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} (g : ApproximableMap (prod V₀ V₁) V₂) : ApproximableMap V₀ (funSpace V₁ V₂)

Theorem 3.12 (Scott 1981, PRG-19). curry(g) : 𝒟₀ → (𝒟₁ → 𝒟₂), where X curry(g) W ↔ (the X-section of g) ∈ W (for W = [Y, Z] this is X ∪ Y g Z).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Domain.Neighborhood.curry_rel {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {g : ApproximableMap (prod V₀ V₁) V₂} {X : Set α} {W : Set (ApproximableMap V₁ V₂)} : (curry g).rel X W ↔ ∃ (hX : V₀.mem X), (funSpace V₁ V₂).mem W ∧ gSection g hX ∈ W

theorem Domain.Neighborhood.toElementMap_curry_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} (g : ApproximableMap (prod V₀ V₁) V₂) (x : V₀.Element) (y : V₁.Element) : (toApproxMap ((curry g).toElementMap x)).toElementMap y = g.toElementMap (pair x y)

Theorem 3.12(i) (Scott 1981, PRG-19). curry(g)(x)(y) = g(x, y).

theorem Domain.Neighborhood.rel_stepFun_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} (h : ApproximableMap V₀ (funSpace V₁ V₂)) {X : Set α} (hX : V₀.mem X) {L : List (Set β × Set γ)} (hL : ∀ p ∈ L, V₁.mem p.1 ∧ V₂.mem p.2) : h.rel X (stepFun L) ↔ ∀ p ∈ L, h.rel X (step p.1 p.2)

The relational generation lemma for maps h : 𝒟₀ → (𝒟₁ → 𝒟₂): X h (⋂ᵢ [Yᵢ,Zᵢ]) iff X h [Yᵢ,Zᵢ] for all i.

theorem Domain.Neighborhood.prod_mem_inl {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {W : Set (α ⊕ β)} (hW : (prod V₀ V₁).mem W) : V₀.mem (Sum.inl ⁻¹' W)

theorem Domain.Neighborhood.prod_mem_inr {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {W : Set (α ⊕ β)} (hW : (prod V₀ V₁).mem W) : V₁.mem (Sum.inr ⁻¹' W)

def Domain.Neighborhood.uncurry {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} (h : ApproximableMap V₀ (funSpace V₁ V₂)) : ApproximableMap (prod V₀ V₁) V₂

Theorem 3.12 (Scott 1981, PRG-19). Uncurrying h : 𝒟₀ → (𝒟₁ → 𝒟₂) to 𝒟₀ × 𝒟₁ → 𝒟₂: X ∪ Y (uncurry h) Z ↔ X h [Y, Z].

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Domain.Neighborhood.uncurry_rel {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {h : ApproximableMap V₀ (funSpace V₁ V₂)} {W : Set (α ⊕ β)} {Z : Set γ} : (uncurry h).rel W Z ↔ (prod V₀ V₁).mem W ∧ h.rel (Sum.inl ⁻¹' W) (step (Sum.inr ⁻¹' W) Z)

theorem Domain.Neighborhood.uncurry_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} (h : ApproximableMap V₀ (funSpace V₁ V₂)) : uncurry h = (evalMap V₁ V₂).comp (paired (h.comp (proj₀ V₀ V₁)) (proj₁ V₀ V₁))

uncurry is the composition eval ∘ ⟨h ∘ p₀, p₁⟩.

theorem Domain.Neighborhood.uncurry_curry {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} (g : ApproximableMap (prod V₀ V₁) V₂) : uncurry (curry g) = g

Theorem 3.12 (Scott 1981, PRG-19). uncurry (curry g) = g.

theorem Domain.Neighborhood.curry_uncurry {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} (h : ApproximableMap V₀ (funSpace V₁ V₂)) : curry (uncurry h) = h

Theorem 3.12 (Scott 1981, PRG-19). curry (uncurry h) = h.

theorem Domain.Neighborhood.eval_comp_curry {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} (g : ApproximableMap (prod V₀ V₁) V₂) : (evalMap V₁ V₂).comp (paired ((curry g).comp (proj₀ V₀ V₁)) (proj₁ V₀ V₁)) = g

Theorem 3.12(ii) (Scott 1981, PRG-19). eval ∘ ⟨curry(g) ∘ p₀, p₁⟩ = g.

theorem Domain.Neighborhood.curry_eval_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} (h : ApproximableMap V₀ (funSpace V₁ V₂)) : curry ((evalMap V₁ V₂).comp (paired (h.comp (proj₀ V₀ V₁)) (proj₁ V₀ V₁))) = h

Theorem 3.12(iii) (Scott 1981, PRG-19). curry (eval ∘ ⟨h ∘ p₀, p₁⟩) = h.

def Domain.Neighborhood.curryEquiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) (V₂ : NeighborhoodSystem γ) : ApproximableMap (prod V₀ V₁) V₂ ≃o ApproximableMap V₀ (funSpace V₁ V₂)

Theorem 3.12 (Scott 1981, PRG-19). curry is an order-isomorphism between |𝒟₀ × 𝒟₁ → 𝒟₂| and |𝒟₀ → (𝒟₁ → 𝒟₂)|.

Equations

• Domain.Neighborhood.curryEquiv V₀ V₁ V₂ = { toFun := Domain.Neighborhood.curry, invFun := Domain.Neighborhood.uncurry, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }