preBeth_limit — Mathlib

English

For o, if ho is a successor-prelimit, then preBeth(o) equals the supremum of preBeth at elements below o.

Русский

Для o, если ho является пределом на следующем шаге, то preBeth(o) равна наибольшему верхнему пределу значений preBeth ниже o.

LaTeX

$$preBeth(o) = \big(\sup a : Iio(o), preBeth(a)\big)$$

Lean4

theorem preBeth_limit {o : Ordinal} (ho : IsSuccPrelimit o) : preBeth o = ⨆ a : Iio o, preBeth a :=
  by
  rw [preBeth]
  apply (ciSup_mono (bddAbove_of_small _) fun _ ↦ (cantor _).le).antisymm'
  rw [ciSup_le_iff' (bddAbove_of_small _)]
  intro a
  rw [← preBeth_succ]
  exact le_ciSup (bddAbove_of_small _) (⟨_, ho.succ_lt a.2⟩ : Iio o)

Похожие утверждения