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.instTopologicalSpaceOrdinal : TopologicalSpace Ordinal.{u}

instance Ordinal.instOrderTopologyOrdinalInstTopologicalSpaceOrdinalToPreorderPartialOrder : OrderTopology Ordinal.{u}

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

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) : Filter.HasBasis (nhds a) (fun x => x < a) fun x => Set.Ioc x a

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

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

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

theorem Ordinal.mem_closure_iff_sup {s : Set Ordinal.{u}} {a : Ordinal.{u}} : a ∈ closure s ↔ ∃ ι x f, (∀ (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 ↔ ∃ ι _hι f, (∀ (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 _ho f, (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) ∧ Ordinal.bsup o f = a

theorem Ordinal.mem_closed_iff_bsup {s : Set Ordinal.{u}} {a : Ordinal.{u}} (hs : IsClosed s) : a ∈ s ↔ ∃ o _ho f, (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) ∧ Ordinal.bsup o 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) → Ordinal.bsup o f ∈ s

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

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 => x < x_1) s) : Ordinal.IsNormal (Ordinal.enumOrd s) ↔ IsClosed s