Lecture III (§3) — the product system: Definitions 3.1, 3.3, Propositions 3.2,

3.4, Lemma 3.6, Theorems 3.5, 3.7

Following Dana Scott, Lectures on a Mathematical Theory of Computation, PRG-19 (1981), Lecture III, Constructions on domains. Given two neighbourhood systems over disjoint token sets Δ₀, Δ₁, the product system 𝒟₀ × 𝒟₁ has neighbourhoods X ∪ Y (X ∈ 𝒟₀, Y ∈ 𝒟₁) over Δ₀ ∪ Δ₁.

We model the disjoint union of token sets by the sum type α ⊕ β, and the product neighbourhood X ∪ Y by prodNbhd X Y = Sum.inl '' X ∪ Sum.inr '' Y. Because Sum.inl and Sum.inr have disjoint ranges, the cleanest facts of Scott's proof become transparent:

• prodNbhd_inter — (X ∪ Y) ∩ (X' ∪ Y') = (X ∩ X') ∪ (Y ∩ Y') (Scott's (2));
• prodNbhd_subset_iff — X ∪ Y ⊆ X' ∪ Y' ↔ X ⊆ X' ∧ Y ⊆ Y' (Scott's (1));
• prodNbhd_injective — the representation X ∪ Y is unique.

This file formalizes:

• Definition 3.1 / Proposition 3.2 — the product system prod V₀ V₁, the element pairing pair x y = ⟨x, y⟩, the order law pair_le_pair_iff (3.2(i)), and the order-isomorphism prodEquiv : |𝒟₀ × 𝒟₁| ≃o |𝒟₀| × |𝒟₁|.
• Definition 3.3 / Proposition 3.4 — projections proj₀, proj₁, the paired mapping paired f g, and proj₀_comp_paired, proj₁_comp_paired, paired_proj (⟨p₀∘h, p₁∘h⟩ = h), toElementMap_paired (⟨f, g⟩(w) = ⟨f(w), g(w)⟩).
• Lemma 3.6 — constant maps constMap b (X b Y ↔ Y ∈ b) with toElementMap_constMap.
• Theorem 3.5 — joint vs. separate approximability, via the bridge ApproximableMap (prod V₀ V₁) V₂ ≃ ApproximableMap₂ V₀ V₁ V₂ (ofMap₂ / toMap₂ and round-trips).
• Proposition 3.7 — multivariate approximable functions are closed under substitution (comp/paired/proj bookkeeping).

Everything is choice-free (#print axioms ⊆ {propext, Quot.sound}).

def Domain.Neighborhood.prodNbhd {α : Type u_1} {β : Type u_2} (X : Set α) (Y : Set β) : Set (α ⊕ β)

The product neighbourhood X ∪ Y over the disjoint union Δ₀ ∪ Δ₁, modelled on α ⊕ β as Sum.inl '' X ∪ Sum.inr '' Y.

Equations

• Domain.Neighborhood.prodNbhd X Y = Sum.inl '' X ∪ Sum.inr '' Y

@[simp]

theorem Domain.Neighborhood.mem_prodNbhd_inl {α : Type u_1} {β : Type u_2} {X : Set α} {Y : Set β} {a : α} : Sum.inl a ∈ prodNbhd X Y ↔ a ∈ X

@[simp]

theorem Domain.Neighborhood.mem_prodNbhd_inr {α : Type u_1} {β : Type u_2} {X : Set α} {Y : Set β} {b : β} : Sum.inr b ∈ prodNbhd X Y ↔ b ∈ Y

@[simp]

theorem Domain.Neighborhood.inl_preimage_prodNbhd {α : Type u_1} {β : Type u_2} (X : Set α) (Y : Set β) : Sum.inl ⁻¹' prodNbhd X Y = X

@[simp]

theorem Domain.Neighborhood.inr_preimage_prodNbhd {α : Type u_1} {β : Type u_2} (X : Set α) (Y : Set β) : Sum.inr ⁻¹' prodNbhd X Y = Y

theorem Domain.Neighborhood.prodNbhd_inter {α : Type u_1} {β : Type u_2} (X X' : Set α) (Y Y' : Set β) : prodNbhd X Y ∩ prodNbhd X' Y' = prodNbhd (X ∩ X') (Y ∩ Y')

Scott's (2): the product nbhds intersect componentwise.

theorem Domain.Neighborhood.prodNbhd_subset_iff {α : Type u_1} {β : Type u_2} {X X' : Set α} {Y Y' : Set β} : prodNbhd X Y ⊆ prodNbhd X' Y' ↔ X ⊆ X' ∧ Y ⊆ Y'

Scott's (1): inclusion of product nbhds is componentwise (uses disjointness of Δ₀, Δ₁).

theorem Domain.Neighborhood.prodNbhd_injective {α : Type u_1} {β : Type u_2} {X X' : Set α} {Y Y' : Set β} (h : prodNbhd X Y = prodNbhd X' Y') : X = X' ∧ Y = Y'

The representation X ∪ Y is unique (choice-free, via the preimage projections).

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

Definition 3.1 (Scott 1981, PRG-19). The product system 𝒟₀ × 𝒟₁: neighbourhoods are X ∪ Y with X ∈ 𝒟₀, Y ∈ 𝒟₁. Closure under consistent intersection is Scott's (2) (prodNbhd_inter) together with the factors' closure; the consistency witness Z ⊆ (X∪Y) ∩ (X'∪Y') splits into witnesses Z₀ ⊆ X ∩ X', Z₁ ⊆ Y ∩ Y' by prodNbhd_subset_iff.

Equations

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

@[simp]

theorem Domain.Neighborhood.prod_mem_iff {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {W : Set (α ⊕ β)} : (prod V₀ V₁).mem W ↔ ∃ (X : Set α), ∃ (Y : Set β), V₀.mem X ∧ V₁.mem Y ∧ W = prodNbhd X Y

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

@[simp]

theorem Domain.Neighborhood.prod_master {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} : (prod V₀ V₁).master = prodNbhd V₀.master V₁.master

Projections of an element (Scott's z₀, z₁).

def Domain.Neighborhood.NeighborhoodSystem.Element.fst {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (z : (prod V₀ V₁).Element) : V₀.Element

Scott's z₀ = {X ∈ 𝒟₀ ∣ X ∪ Δ₁ ∈ z}: the first component of a product element.

Equations

• z.fst = { mem := fun (X : Set α) => V₀.mem X ∧ z.mem (Domain.Neighborhood.prodNbhd X V₁.master), sub := ⋯, master_mem := ⋯, inter_mem := ⋯, up_mem := ⋯ }

def Domain.Neighborhood.NeighborhoodSystem.Element.snd {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (z : (prod V₀ V₁).Element) : V₁.Element

Scott's z₁ = {Y ∈ 𝒟₁ ∣ Δ₀ ∪ Y ∈ z}: the second component of a product element.

Equations

• z.snd = { mem := fun (Y : Set β) => V₁.mem Y ∧ z.mem (Domain.Neighborhood.prodNbhd V₀.master Y), sub := ⋯, master_mem := ⋯, inter_mem := ⋯, up_mem := ⋯ }

@[simp]

theorem Domain.Neighborhood.mem_fst {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {z : (prod V₀ V₁).Element} {X : Set α} : z.fst.mem X ↔ V₀.mem X ∧ z.mem (prodNbhd X V₁.master)

@[simp]

theorem Domain.Neighborhood.mem_snd {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {z : (prod V₀ V₁).Element} {Y : Set β} : z.snd.mem Y ↔ V₁.mem Y ∧ z.mem (prodNbhd V₀.master Y)

theorem Domain.Neighborhood.prod_mem_split {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {z : (prod V₀ V₁).Element} {X : Set α} {Y : Set β} (hX : V₀.mem X) (hY : V₁.mem Y) : z.mem (prodNbhd X Y) ↔ z.mem (prodNbhd X V₁.master) ∧ z.mem (prodNbhd V₀.master Y)

The key splitting (Scott's (3)): for a product element z and neighbourhoods X ∈ 𝒟₀, Y ∈ 𝒟₁, membership of X ∪ Y in z is equivalent to membership of its two "slices".

Definition 3.1 — the element pairing ⟨x, y⟩.

def Domain.Neighborhood.pair {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (x : V₀.Element) (y : V₁.Element) : (prod V₀ V₁).Element

Definition 3.1 (Scott 1981, PRG-19). The element pairing ⟨x, y⟩ = {X ∪ Y ∣ X ∈ x, Y ∈ y}.

Equations

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

@[simp]

theorem Domain.Neighborhood.mem_pair {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {x : V₀.Element} {y : V₁.Element} {W : Set (α ⊕ β)} : (pair x y).mem W ↔ ∃ (X : Set α), ∃ (Y : Set β), x.mem X ∧ y.mem Y ∧ W = prodNbhd X Y

theorem Domain.Neighborhood.mem_pair_prodNbhd {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {x : V₀.Element} {y : V₁.Element} {X : Set α} {Y : Set β} : (pair x y).mem (prodNbhd X Y) ↔ x.mem X ∧ y.mem Y

theorem Domain.Neighborhood.pair_le_pair_iff {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {x x' : V₀.Element} {y y' : V₁.Element} : pair x y ≤ pair x' y' ↔ x ≤ x' ∧ y ≤ y'

Proposition 3.2(i) (Scott 1981, PRG-19). ⟨x, y⟩ ⊑ ⟨x', y'⟩ ↔ x ⊑ x' ∧ y ⊑ y'.

theorem Domain.Neighborhood.pair_fst_snd {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (z : (prod V₀ V₁).Element) : pair z.fst z.snd = z

z = ⟨z₀, z₁⟩: every product element is the pairing of its two components.

@[simp]

theorem Domain.Neighborhood.fst_pair {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (x : V₀.Element) (y : V₁.Element) : (pair x y).fst = x

@[simp]

theorem Domain.Neighborhood.snd_pair {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (x : V₀.Element) (y : V₁.Element) : (pair x y).snd = y

def Domain.Neighborhood.prodEquiv {α : Type u_1} {β : Type u_2} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) : (prod V₀ V₁).Element ≃o V₀.Element × V₁.Element

Proposition 3.2 (Scott 1981, PRG-19). The order-isomorphism |𝒟₀ × 𝒟₁| ≃o |𝒟₀| × |𝒟₁|.

Equations

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

@[simp]

theorem Domain.Neighborhood.prodEquiv_apply {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (z : (prod V₀ V₁).Element) : (prodEquiv V₀ V₁) z = (z.fst, z.snd)

@[simp]

theorem Domain.Neighborhood.prodEquiv_symm_apply {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (p : V₀.Element × V₁.Element) : (prodEquiv V₀ V₁).symm p = pair p.1 p.2

Definition 3.3 / Proposition 3.4 — projections and pairing of maps.

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

Every product neighbourhood is (inl⁻¹ W) ∪ (inr⁻¹ W).

theorem Domain.Neighborhood.ApproximableMap.rel_master {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (f : ApproximableMap V₀ V₁) {X : Set α} (hX : V₀.mem X) : f.rel X V₁.master

An approximable map relates any input neighbourhood to the master output Δ₁.

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

Definition 3.3 (Scott 1981, PRG-19). The projection p₀ : 𝒟₀ × 𝒟₁ → 𝒟₀, (X ∪ Y) p₀ X' ↔ X ⊆ X'.

Equations

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

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

Definition 3.3 (Scott 1981, PRG-19). The projection p₁ : 𝒟₀ × 𝒟₁ → 𝒟₁, (X ∪ Y) p₁ Y' ↔ Y ⊆ Y'.

Equations

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

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

Definition 3.3 (Scott 1981, PRG-19). The paired mapping ⟨f, g⟩ : 𝒟₂ → 𝒟₀ × 𝒟₁, Z ⟨f, g⟩ (X ∪ Y) ↔ Z f X ∧ Z g Y.

Equations

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

@[simp]

theorem Domain.Neighborhood.proj₀_rel {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {W : Set (α ⊕ β)} {X' : Set α} : (proj₀ V₀ V₁).rel W X' ↔ (prod V₀ V₁).mem W ∧ V₀.mem X' ∧ Sum.inl ⁻¹' W ⊆ X'

@[simp]

theorem Domain.Neighborhood.proj₁_rel {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {W : Set (α ⊕ β)} {Y' : Set β} : (proj₁ V₀ V₁).rel W Y' ↔ (prod V₀ V₁).mem W ∧ V₁.mem Y' ∧ Sum.inr ⁻¹' W ⊆ Y'

@[simp]

theorem Domain.Neighborhood.paired_rel {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {f : ApproximableMap V₂ V₀} {g : ApproximableMap V₂ V₁} {Z : Set γ} {P : Set (α ⊕ β)} : (paired f g).rel Z P ↔ (prod V₀ V₁).mem P ∧ f.rel Z (Sum.inl ⁻¹' P) ∧ g.rel Z (Sum.inr ⁻¹' P)

@[simp]

theorem Domain.Neighborhood.toElementMap_proj₀ {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (z : (prod V₀ V₁).Element) : (proj₀ V₀ V₁).toElementMap z = z.fst

Proposition 3.4(ii) (Scott 1981, PRG-19). p₀(z) = z₀.

@[simp]

theorem Domain.Neighborhood.toElementMap_proj₁ {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (z : (prod V₀ V₁).Element) : (proj₁ V₀ V₁).toElementMap z = z.snd

Proposition 3.4(ii) (Scott 1981, PRG-19). p₁(z) = z₁.

theorem Domain.Neighborhood.toElementMap_paired {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} (f : ApproximableMap V₂ V₀) (g : ApproximableMap V₂ V₁) (w : V₂.Element) : (paired f g).toElementMap w = pair (f.toElementMap w) (g.toElementMap w)

Proposition 3.4(iv) (Scott 1981, PRG-19). ⟨f, g⟩(w) = ⟨f(w), g(w)⟩.

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

Proposition 3.4(i) (Scott 1981, PRG-19). p₀ ∘ ⟨f, g⟩ = f.

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

Proposition 3.4(i) (Scott 1981, PRG-19). p₁ ∘ ⟨f, g⟩ = g.

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

Proposition 3.4(iii) (Scott 1981, PRG-19). h = ⟨p₀ ∘ h, p₁ ∘ h⟩.

theorem Domain.Neighborhood.prod_mem_prodNbhd_iff {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {X : Set α} {Y : Set β} : (prod V₀ V₁).mem (prodNbhd X Y) ↔ V₀.mem X ∧ V₁.mem Y

Lemma 3.6 — constant maps.

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

Lemma 3.6 (Scott 1981, PRG-19). The constant map at b : |𝒟₁|: X b Y ↔ Y ∈ b.

Equations

• Domain.Neighborhood.constMap V₀ b = { rel := fun (X : Set α) (Y : Set β) => V₀.mem X ∧ b.mem Y, rel_dom := ⋯, rel_cod := ⋯, master_rel := ⋯, inter_right := ⋯, mono := ⋯ }

@[simp]

theorem Domain.Neighborhood.constMap_rel {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {b : V₁.Element} {X : Set α} {Y : Set β} : (constMap V₀ b).rel X Y ↔ V₀.mem X ∧ b.mem Y

@[simp]

theorem Domain.Neighborhood.toElementMap_constMap {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (b : V₁.Element) (x : V₀.Element) : (constMap V₀ b).toElementMap x = b

Lemma 3.6 (Scott 1981, PRG-19). The constant map sends every element to b.

Theorem 3.5 — joint vs. separate approximability.

theorem Domain.Neighborhood.ApproximableMap₂.ext {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {f g : ApproximableMap₂ V₀ V₁ V₂} (h : ∀ (X : Set α) (Y : Set β) (Z : Set γ), f.rel X Y Z ↔ g.rel X Y Z) : f = g

Extensionality for two-variable approximable mappings.

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

Theorem 3.5 (→) (Scott 1981, PRG-19). A joint approximable mapping 𝒟₀ × 𝒟₁ → 𝒟₂ restricts to a two-variable mapping X, Y f Z ↔ (X ∪ Y) f Z.

Equations

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

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

Theorem 3.5 (←) (Scott 1981, PRG-19). A two-variable mapping induces a joint mapping.

Equations

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

theorem Domain.Neighborhood.toMap₂_ofMap₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} (f : ApproximableMap₂ V₀ V₁ V₂) : toMap₂ (ofMap₂ f) = f

theorem Domain.Neighborhood.ofMap₂_toMap₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} (f : ApproximableMap (prod V₀ V₁) V₂) : ofMap₂ (toMap₂ f) = f

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

Theorem 3.5 (Scott 1981, PRG-19). The bijection between joint approximable mappings 𝒟₀ × 𝒟₁ → 𝒟₂ and two-variable mappings 𝒟₀, 𝒟₁ → 𝒟₂: a function of two arguments comes from an approximable mapping iff it is separately approximable.

Equations

• Domain.Neighborhood.map₂Equiv V₀ V₁ V₂ = { toFun := Domain.Neighborhood.toMap₂, invFun := Domain.Neighborhood.ofMap₂, left_inv := ⋯, right_inv := ⋯ }

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

Theorem 3.5 (elementwise) (Scott 1981, PRG-19). The two-variable elementwise map of toMap₂ f is f evaluated at the pairing: (toMap₂ f)(x, y) = f(⟨x, y⟩).

Proposition 3.7 — closure under substitution.

theorem Domain.Neighborhood.substitution_toElementMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {V₃ : NeighborhoodSystem δ} (F : ApproximableMap (prod V₀ V₁) V₂) (a : ApproximableMap V₃ V₀) (b : ApproximableMap V₃ V₁) (w : V₃.Element) : (F.comp (paired a b)).toElementMap w = (toMap₂ F).toElementMap₂ (a.toElementMap w) (b.toElementMap w)

Proposition 3.7 (Scott 1981, PRG-19). Multivariate approximable functions are closed under substitution: substituting approximable maps a, b : 𝒟₃ → 𝒟ᵢ into a two-variable approximable map F : 𝒟₀ × 𝒟₁ → 𝒟₂ yields the approximable map F ∘ ⟨a, b⟩, whose value is F(a(w), b(w)). The building blocks are exactly Definition 3.3's paired and Theorem 2.5's comp.