English
For s ⊆ Ordinal, Open(s) iff for every o ∈ s with IsSuccLimit(o) there exists a < o with Ioo(a,o) ⊆ s.
Русский
Для подмножества s ⊆ Ordinal: открытость эквивалентна существованию for каждого o ∈ s, если IsSuccLimit(o), тогда ∃ a < o: Ioo(a,o) ⊆ s.
LaTeX
$$$\forall s \subseteq \mathrm{Ordinal},\ \text{IsOpen}(s) \iff \forall o \in s,\ \text{IsSuccLimit}(o) \rightarrow \exists a < o,\ \mathrm{Ioo}(a,o) \subseteq s$$$
Lean4
theorem isOpen_iff : IsOpen s ↔ ∀ o ∈ s, IsSuccLimit o → ∃ a < o, Set.Ioo a o ⊆ s :=
by
refine isOpen_iff_mem_nhds.trans <| forall₂_congr fun o ho => ?_
by_cases ho' : IsSuccLimit o
· simp only [(SuccOrder.hasBasis_nhds_Ioc_of_exists_lt ⟨0, ho'.bot_lt⟩).mem_iff, ho', true_implies]
refine exists_congr fun a => and_congr_right fun ha => ?_
simp only [← Set.Ioo_insert_right ha, Set.insert_subset_iff, ho, true_and]
· simp [nhds_eq_pure.2 ho', ho, ho']
