lt_opow_of_isSuccLimit — Mathlib

English

If b ≠ 0 and c is a successor-limit, then a < b^c iff there exists c' < c with a < b^c'.

Русский

Если b ≠ 0 и c является предельной степенью типа следования, то a < b^c тогда и только тогда, когда существует c' < c such that a < b^c'.

LaTeX

$$$\forall a,b,c : \mathrm{Ordinal},\ b \ne 0 \land \mathrm{IsSuccLimit}(c) \Rightarrow a < b^c \iff \exists c' < c,\ a < b^{c'}$$$

Lean4

theorem lt_opow_of_isSuccLimit {a b c : Ordinal} (b0 : b ≠ 0) (h : IsSuccLimit c) : a < b ^ c ↔ ∃ c' < c, a < b ^ c' :=
  by simpa using (opow_le_of_isSuccLimit b0 h).not

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