log_eq_iff — Mathlib

English

Let hb: 1 < b and hx: x ≠ 0. For any y, log_b x = y if and only if b^y ≤ x and x < b^{succ y}.

Русский

Пусть hb: 1 < b и hx: x ≠ 0. Тогда log_b x = y тогда и только тогда b^y ≤ x и x < b^{succ y}.

LaTeX

$$$ \log_b x = y \iff b^y \le x \land x < b^{\operatorname{succ} y} $$$

Lean4

theorem log_eq_iff {b x : Ordinal} (hb : 1 < b) (hx : x ≠ 0) (y : Ordinal) : log b x = y ↔ b ^ y ≤ x ∧ x < b ^ succ y :=
  by
  constructor
  · rintro rfl
    use opow_log_le_self b hx, lt_opow_succ_log_self hb x
  · rintro ⟨hx₁, hx₂⟩
    apply le_antisymm
    · rwa [← lt_succ_iff, ← lt_opow_iff_log_lt hb hx]
    · rwa [← opow_le_iff_le_log hb hx]

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