English
Let S be a set of ordinals with no upper bound. The enumeration map of S is a normal function if and only if S is closed.
Русский
Пусть S — множество ординалов без верхней границы. Отображение перечисления enumOrd(S) нормально тогда и только тогда, когда S замкнуто.
LaTeX
$$$\neg \mathrm{BddAbove}(S) \Rightarrow \bigl( \mathrm{IsNormal}(\mathrm{enumOrd}(S)) \iff \mathrm{IsClosed}(S) \bigr)$$$
Lean4
theorem enumOrd_isNormal_iff_isClosed (hs : ¬BddAbove s) : IsNormal (enumOrd s) ↔ IsClosed s :=
by
have Hs := enumOrd_strictMono hs
refine
⟨fun h => isClosed_iff_iSup.2 fun {ι} hι f hf => ?_, fun h =>
(isNormal_iff_strictMono_limit _).2 ⟨Hs, fun a ha o H => ?_⟩⟩
· let g : ι → Ordinal.{u} := fun i => (enumOrdOrderIso s hs).symm ⟨_, hf i⟩
suffices enumOrd s (⨆ i, g i) = ⨆ i, f i by
rw [← this]
exact enumOrd_mem hs _
rw [IsNormal.map_iSup h g]
congr
ext x
change (enumOrdOrderIso s hs _).val = f x
rw [OrderIso.apply_symm_apply]
· rw [isClosed_iff_bsup] at h
suffices enumOrd s a ≤ bsup.{u, u} a fun b (_ : b < a) => enumOrd s b from this.trans (bsup_le H)
obtain ⟨b, hb⟩ := enumOrd_surjective hs (h ha.ne_bot (fun b _ => enumOrd s b) fun b _ => enumOrd_mem hs b)
rw [← hb]
apply Hs.monotone
by_contra! hba
apply (Hs (lt_succ b)).not_ge
rw [hb]
exact le_bsup.{u, u} _ _ (ha.succ_lt hba)
