Topology of ordinals

We prove some miscellaneous results involving the order topology of ordinals.

Main results

• Ordinal.isClosed_iff_sup / Ordinal.isClosed_iff_bsup: A set of ordinals is closed iff it's closed under suprema.
• Ordinal.isNormal_iff_strictMono_and_continuous: A characterization of normal ordinal functions.
• Ordinal.enumOrd_isNormal_iff_isClosed: The function enumerating the ordinals of a set is normal iff the set is closed.

instance Ordinal.instTopologicalSpace : TopologicalSpace Ordinal.{u}

Equations

• Ordinal.instTopologicalSpace = Preorder.topology Ordinal.{u}

instance Ordinal.instOrderTopology : OrderTopology Ordinal.{u}

Equations

• Ordinal.instOrderTopology = ⋯

theorem Ordinal.isOpen_singleton_iff {a : Ordinal.{u}} : IsOpen {a} ↔ ¬a.IsLimit

theorem Ordinal.nhds_right' (a : Ordinal.{u_1}) : nhdsWithin a (Set.Ioi a) = ⊥

theorem Ordinal.nhds_left'_eq_nhds_ne (a : Ordinal.{u_1}) : nhdsWithin a (Set.Iio a) = nhdsWithin a {a}ᶜ

theorem Ordinal.nhds_left_eq_nhds (a : Ordinal.{u_1}) : nhdsWithin a (Set.Iic a) = nhds a

theorem Ordinal.nhdsBasis_Ioc {a : Ordinal.{u}} (h : a ≠ 0) : (nhds a).HasBasis (fun (x : Ordinal.{u}) => x < a) fun (x : Ordinal.{u}) => Set.Ioc x a

theorem Ordinal.nhds_eq_pure {a : Ordinal.{u}} : nhds a = pure a ↔ ¬a.IsLimit

theorem Ordinal.isOpen_iff {s : Set Ordinal.{u}} : IsOpen s ↔ ∀ o ∈ s, o.IsLimit → ∃ a < o, Set.Ioo a o ⊆ s

theorem Ordinal.mem_closure_tfae (a : Ordinal.{u}) (s : Set Ordinal.{u}) : [a ∈ closure s, a ∈ closure (s ∩ Set.Iic a), (s ∩ Set.Iic a).Nonempty ∧ sSup (s ∩ Set.Iic a) = a, ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a, ∃ (o : Ordinal.{u}), o ≠ 0 ∧ ∃ (f : (x : Ordinal.{u}) → x < o → Ordinal.{u}), (∀ (x : Ordinal.{u}) (hx : x < o), f x hx ∈ s) ∧ o.bsup f = a, ∃ (ι : Type u), Nonempty ι ∧ ∃ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) ∧ Ordinal.sup f = a].TFAE

theorem Ordinal.mem_closure_iff_sup {s : Set Ordinal.{u}} {a : Ordinal.{u}} : a ∈ closure s ↔ ∃ (ι : Type u) (_ : Nonempty ι) (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) ∧ Ordinal.sup f = a

theorem Ordinal.mem_closed_iff_sup {s : Set Ordinal.{u}} {a : Ordinal.{u}} (hs : IsClosed s) : a ∈ s ↔ ∃ (ι : Type u) (_ : Nonempty ι) (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) ∧ Ordinal.sup f = a

theorem Ordinal.mem_closure_iff_bsup {s : Set Ordinal.{u}} {a : Ordinal.{u}} : a ∈ closure s ↔ ∃ (o : Ordinal.{u}) (_ : o ≠ 0) (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) ∧ o.bsup f = a

theorem Ordinal.mem_closed_iff_bsup {s : Set Ordinal.{u}} {a : Ordinal.{u}} (hs : IsClosed s) : a ∈ s ↔ ∃ (o : Ordinal.{u}) (_ : o ≠ 0) (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) ∧ o.bsup f = a

theorem Ordinal.isClosed_iff_sup {s : Set Ordinal.{u}} : IsClosed s ↔ ∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → Ordinal.sup f ∈ s

theorem Ordinal.isClosed_iff_bsup {s : Set Ordinal.{u}} : IsClosed s ↔ ∀ {o : Ordinal.{u}}, o ≠ 0 → ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → o.bsup f ∈ s

theorem Ordinal.isLimit_of_mem_frontier {s : Set Ordinal.{u}} {a : Ordinal.{u}} (ha : a ∈ frontier s) : a.IsLimit

theorem Ordinal.isNormal_iff_strictMono_and_continuous (f : Ordinal.{u} → Ordinal.{u}) : Ordinal.IsNormal f ↔ StrictMono f ∧ Continuous f

theorem Ordinal.enumOrd_isNormal_iff_isClosed {s : Set Ordinal.{u}} (hs : Set.Unbounded (fun (x x_1 : Ordinal.{u}) => x < x_1) s) : Ordinal.IsNormal (Ordinal.enumOrd s) ↔ IsClosed s