English
For b > 1 and x ≠ 0, succ(log b x) equals the infimum of { o : x < b^o }.
Русский
Для b > 1 и x ≠ 0,succ(log_b x) равно инфимума множества { o : x < b^o }.
LaTeX
$$$\forall b,x \in \mathrm{Ordinal},\ b > 1 \land x \neq 0 \Rightarrow \operatorname{succ}(\log b x) = \inf\{o : x < b^{o}\}$$$
Lean4
theorem succ_log_def {b x : Ordinal} (hb : 1 < b) (hx : x ≠ 0) : succ (log b x) = sInf {o : Ordinal | x < b ^ o} :=
by
let t := sInf {o : Ordinal | x < b ^ o}
have : x < b ^ t := csInf_mem (log_nonempty hb)
rcases zero_or_succ_or_isSuccLimit t with (h | h | h)
· refine ((one_le_iff_ne_zero.2 hx).not_gt ?_).elim
simpa only [h, opow_zero] using this
· rw [log_def hb x, succ_pred_eq_iff_not_isSuccPrelimit, not_isSuccPrelimit_iff']
simpa [eq_comm] using h
· rcases (lt_opow_of_isSuccLimit (zero_lt_one.trans hb).ne' h).1 this with ⟨a, h₁, h₂⟩
exact h₁.not_ge.elim ((le_csInf_iff'' (log_nonempty hb)).1 le_rfl a h₂)
