English
For every ordinal o, the cardinal preBeth(o) is a strong limit cardinal if and only if o is a successor-limit ordinal.
Русский
Для каждого ординала o кардинал preBeth(o) является сильным пределом тогда и только тогда, когда o является succ‑пределным ординалом.
LaTeX
$$$\operatorname{IsStrongLimit}(\mathrm{preBeth}(o)) \iff \operatorname{IsSuccLimit}(o)$$$
Lean4
theorem isStrongLimit_preBeth {o : Ordinal} : IsStrongLimit (preBeth o) ↔ IsSuccLimit o :=
by
by_cases H : IsSuccLimit o
· refine iff_of_true ⟨by simpa using H.ne_bot, fun a ha ↦ ?_⟩ H
rw [preBeth_limit H.isSuccPrelimit] at ha
rcases exists_lt_of_lt_ciSup' ha with ⟨⟨i, hi⟩, ha⟩
have := power_le_power_left two_ne_zero ha.le
rw [← preBeth_succ] at this
exact this.trans_lt (preBeth_strictMono (H.succ_lt hi))
· apply iff_of_false _ H
rw [not_isSuccLimit_iff, not_isSuccPrelimit_iff'] at H
obtain ho | ⟨a, rfl⟩ := H
· simp [ho.eq_bot]
· intro h
simpa using h.two_power_lt (preBeth_strictMono (lt_succ a))
