mathlib3 documentation

set_theory.ordinal.topology

Topology of ordinals #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main results #

source
@[protected, instance]
def ordinal.topological_space  :
topological_space ordinal
Equations
source
@[protected, instance]
def ordinal.order_topology  :
order_topology ordinal
source
theorem ordinal.is_open_singleton_iff {a : ordinal} :
is_open {a} ↔ ¬a.is_limit
source
theorem ordinal.is_open_iff {s : set ordinal} :
is_open s ↔ ∀ (o : ordinal), o ∈ s → o.is_limit → (∃ (a : ordinal) (H : a < o), set.Ioo a o ⊆ s)
source
theorem ordinal.mem_closure_iff_sup {s : set ordinal} {a : ordinal} :
a ∈ closure s ↔ ∃ {ι : Type u} [_inst_1 : nonempty ι] (f : ι → ordinal), (∀ (i : ι), f i ∈ s) ∧ ordinal.sup f = a
source
theorem ordinal.mem_closed_iff_sup {s : set ordinal} {a : ordinal} (hs : is_closed s) :
a ∈ s ↔ ∃ {ι : Type u} (hι : nonempty ι) (f : ι → ordinal), (∀ (i : ι), f i ∈ s) ∧ ordinal.sup f = a
source
theorem ordinal.mem_closure_iff_bsup {s : set ordinal} {a : ordinal} :
a ∈ closure s ↔ ∃ {o : ordinal} (ho : o ≠ 0) (f : Π (a : ordinal), a < o → ordinal), (∀ (i : ordinal) (hi : i < o), f i hi ∈ s) ∧ o.bsup f = a
source
theorem ordinal.mem_closed_iff_bsup {s : set ordinal} {a : ordinal} (hs : is_closed s) :
a ∈ s ↔ ∃ {o : ordinal} (ho : o ≠ 0) (f : Π (a : ordinal), a < o → ordinal), (∀ (i : ordinal) (hi : i < o), f i hi ∈ s) ∧ o.bsup f = a
source
theorem ordinal.is_closed_iff_sup {s : set ordinal} :
is_closed s ↔ ∀ {ι : Type u}, nonempty ι → ∀ (f : ι → ordinal), (∀ (i : ι), f i ∈ s) → ordinal.sup f ∈ s
source
theorem ordinal.is_closed_iff_bsup {s : set ordinal} :
is_closed s ↔ ∀ {o : ordinal}, o ≠ 0 → ∀ (f : Π (a : ordinal), a < o → ordinal), (∀ (i : ordinal) (hi : i < o), f i hi ∈ s) → o.bsup f ∈ s
source
theorem ordinal.is_limit_of_mem_frontier {s : set ordinal} {a : ordinal} (ha : a ∈ frontier s) :
a.is_limit
source
theorem ordinal.is_normal_iff_strict_mono_and_continuous (f : ordinal → ordinal) :
ordinal.is_normal f ↔ strict_mono f ∧ continuous f
source
theorem ordinal.enum_ord_is_normal_iff_is_closed {s : set ordinal} (hs : set.unbounded has_lt.lt s) :
ordinal.is_normal (ordinal.enum_ord s) ↔ is_closed s