Exercise 2.13 (Scott 1981, PRG-19, §2) — approximable maps are the

continuous functions

EXERCISE 2.13. (For topologists.) Recall Exercise 1.22 where it was shown that any domain |𝒟| is a topological space. Prove from Exercise 2.9 that the functions f : |𝒟₀| → |𝒟₁| determined by approximable mappings are exactly the continuous functions between these spaces.

This file closes the loop between the §2 theory of approximable mappings (Approximable.lean, ApproximableExercises.lean) and the Exercise 1.22 topology on |𝒟| (Exercise122.lean):

• continuous_toElementMap — every approximable mapping f induces a continuous function x ↦ f(x). Scott's hint: by Exercise 2.9, f⁻¹[Y] = ⋃ {[X] ∣ Y ∈ f(↑X)}, so the inverse image of a basic open is a union of basic opens, hence open.
• continuous_monotone — a continuous c : |𝒟₀| → |𝒟₁| is monotone for ⊑ (the order is the specialization order, le_iff_isOpen_imp).
• mem_iff_principal_of_continuous — Scott's union formula for a continuous c: Y ∈ c(x) ↔ ∃ X ∈ x, Y ∈ c(↑X). (Forward: c⁻¹[X] open ∋ x; reverse: ↑X ⊑ x + monotone.)
• ofContinuous — the approximable mapping of a continuous function, built from ofMono on the finite elements ↑X ↦ c(↑X) (monotone by continuous_monotone).
• toElementMap_ofContinuous — the round trip: ofContinuous c hc induces exactly c ((ofContinuous c hc)(x) = c(x)), combining Exercise 2.9 with the union formula.

Together: f ↦ toElementMap f and c ↦ ofContinuous c exhibit approximable mappings 𝒟₀ → 𝒟₁ and continuous functions |𝒟₀| → |𝒟₁| as the same thing.

Choice-free apart from the ofMono/Exercise-2.9 ingredients (whose uniqueness companions are the only classical pieces).

theorem Domain.Neighborhood.ApproximableMap.continuous_toElementMap {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (f : ApproximableMap V₀ V₁) : Continuous fun (x : V₀.Element) => f.toElementMap x

Exercise 2.13 (forward). The elementwise function of an approximable mapping is continuous. For an open U and x with f(x) ∈ U, openness gives Y with Y ∈ f(x) and [Y] ⊆ U; unfolding Y ∈ f(x) produces X ∈ x with X f Y; then [X] ⊆ f⁻¹U, since any x' ∈ [X] has Y ∈ f(x') (via X f Y).

theorem Domain.Neighborhood.NeighborhoodSystem.continuous_monotone {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {c : V₀.Element → V₁.Element} (hc : Continuous c) : Monotone c

A continuous function between domains is monotone for the approximation order ⊑: this is because ⊑ is recoverable from the topology (le_iff_isOpen_imp) and continuous preimages of opens are open and upward closed (isOpen_isUpperSet).

theorem Domain.Neighborhood.NeighborhoodSystem.mem_iff_principal_of_continuous {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {c : V₀.Element → V₁.Element} (hc : Continuous c) (x : V₀.Element) {Y : Set β} : (c x).mem Y ↔ ∃ (X : Set α) (hx : x.mem X), (c (V₀.principal ⋯)).mem Y

Exercise 2.13 — Scott's union formula for a continuous map. For continuous c and any x ∈ |𝒟₀|: Y ∈ c(x) ↔ ∃ X ∈ x, Y ∈ c(↑X).

• → : c⁻¹[[Y]] is open and contains x, so it contains a basic neighbourhood [X] with X ∈ x; since ↑X ∈ [X], Y ∈ c(↑X).
• ← : ↑X ⊑ x and c monotone (continuous_monotone) give c(↑X) ⊑ c(x), transporting Y.

def Domain.Neighborhood.ApproximableMap.ofContinuous {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (c : V₀.Element → V₁.Element) (hc : Continuous c) : ApproximableMap V₀ V₁

Exercise 2.13 (reverse). The approximable mapping determined by a continuous function c: its action on the finite element ↑X is the value c(↑X), extended to all of 𝒟₀ via ofMono. Monotonicity of X ↦ c(↑X) is continuous_monotone together with the inclusion-reversal X' ⊆ X ↔ ↑X ⊑ ↑X'.

Equations

• Domain.Neighborhood.ApproximableMap.ofContinuous c hc = Domain.Neighborhood.ApproximableMap.ofMono (fun (_X : Set α) (hX : V₀.mem _X) => c (V₀.principal hX)) ⋯

theorem Domain.Neighborhood.ApproximableMap.toElementMap_ofContinuous {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (c : V₀.Element → V₁.Element) (hc : Continuous c) (x : V₀.Element) : (ofContinuous c hc).toElementMap x = c x

Exercise 2.13 — the round trip. ofContinuous c hc induces exactly c: (ofContinuous c hc)(x) = c(x) for all x. Exercise 2.9 reduces f(x) to a union over finite approximants ↑X (X ∈ x), where ofMono evaluates to c(↑X); the union formula mem_iff_principal_of_continuous then re-assembles c(x).