Exercise 1.17 (Scott 1981, PRG-19, §1) — rational open intervals on ℝ

Δ = ℝ; 𝒟 = the non-empty open intervals with rational endpoints, plus Δ itself (ratIntervalSystem). The system law (inter_mem) reduces to the fact that the intersection of two rational intervals is empty or again a rational interval (Set.Ioo_inter_Ioo with max/min of the rational endpoints): inter_mem'.

For each real t, filterAt t = {X ∈ 𝒟 ∣ t ∈ X} is a filter (filterAt). These embed ℝ into |𝒟| injectively (filterAt_injective, using rational density), so |𝒟| contains a faithful copy of the reals.

Scope. Scott's full classification of the total elements (the hint: for rational t, intervals with t as a right-hand endpoint give a second total element at t) needs more real analysis and is left to prose; we deliver the system, the point-filters, and their injectivity. This is the first uncountable Δ of the block.

The constructions are [propext, Quot.sound]; injectivity uses exists_rat_btwn (Archimedean, classical).

def Domain.Neighborhood.RatInterval.ratIntervalMem (X : Set ℝ) : Prop

A neighbourhood of ratIntervalSystem: either Δ = ℝ, or a non-empty open interval with rational endpoints.

Equations

• Domain.Neighborhood.RatInterval.ratIntervalMem X = (X = Set.univ ∨ ∃ (a : ℚ) (b : ℚ), a < b ∧ X = Set.Ioo ↑a ↑b)

theorem Domain.Neighborhood.RatInterval.ratIntervalMem_nonempty {X : Set ℝ} (hX : ratIntervalMem X) : X.Nonempty

Every neighbourhood is non-empty (Δ, or Ioo a b with a < b).

theorem Domain.Neighborhood.RatInterval.inter_mem' {X Y : Set ℝ} (hX : ratIntervalMem X) (hY : ratIntervalMem Y) (hne : (X ∩ Y).Nonempty) : ratIntervalMem (X ∩ Y)

Exercise 1.17 — intersections. The intersection of two neighbourhoods that share a point is again a neighbourhood: Ioo a b ∩ Ioo c d = Ioo (max a c) (min b d), with rational endpoints, non-empty because it contains the shared point.

def Domain.Neighborhood.RatInterval.ratIntervalSystem : NeighborhoodSystem ℝ

Exercise 1.17 — the rational-interval neighbourhood system over ℝ.

Equations

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

@[simp]

theorem Domain.Neighborhood.RatInterval.ratIntervalSystem_mem {X : Set ℝ} : ratIntervalSystem.mem X ↔ ratIntervalMem X

def Domain.Neighborhood.RatInterval.filterAt (t : ℝ) : ratIntervalSystem.Element

Exercise 1.17 — the point filter {X ∈ 𝒟 ∣ t ∈ X}. For any real t this is a filter: closure under ∩ uses inter_mem' with t itself as the shared point.

Equations

• Domain.Neighborhood.RatInterval.filterAt t = { mem := fun (X : Set ℝ) => Domain.Neighborhood.RatInterval.ratIntervalMem X ∧ t ∈ X, sub := ⋯, master_mem := ⋯, inter_mem := ⋯, up_mem := ⋯ }

@[simp]

theorem Domain.Neighborhood.RatInterval.mem_filterAt {t : ℝ} {X : Set ℝ} : (filterAt t).mem X ↔ ratIntervalMem X ∧ t ∈ X

theorem Domain.Neighborhood.RatInterval.filterAt_injective {s t : ℝ} (h : filterAt s = filterAt t) : s = t

Exercise 1.17 — ℝ ↪ |𝒟|. Distinct reals give distinct point filters: between any two reals lies a rational interval separating them.