English
A singleton {a} is open in the ordinal topology iff a is not a succ-limit.
Русский
Единственная точка {a} открыта в ординальной топологии тогда и только тогда, когда a не succ-limit.
LaTeX
$$$\text{IsOpen}(\{a\}) \iff \neg \text{IsSuccLimit}(a)$$$
Lean4
theorem isOpen_singleton_iff : IsOpen ({ a } : Set Ordinal) ↔ ¬IsSuccLimit a :=
by
refine ⟨fun h ha => ?_, fun ha => ?_⟩
· obtain ⟨b, c, hbc, hbc'⟩ := (mem_nhds_iff_exists_Ioo_subset' ⟨0, ha.bot_lt⟩ ⟨_, lt_succ a⟩).1 (h.mem_nhds rfl)
have hba := ha.succ_lt hbc.1
exact hba.ne (hbc' ⟨lt_succ b, hba.trans hbc.2⟩)
· rcases zero_or_succ_or_isSuccLimit a with (rfl | ⟨b, rfl⟩ | ha')
· rw [← bot_eq_zero, ← Set.Iic_bot, ← Iio_succ]
exact isOpen_Iio
· rw [← Set.Icc_self, Icc_succ_left, ← Ioo_succ_right]
exact isOpen_Ioo
· exact (ha ha').elim
