one_lt_rpow_iff_of_pos — Mathlib

English

Let x > 0. Then 1 < x^y iff (1 < x ∧ 0 < y) or (x < 1 ∧ y < 0).

Русский

Пусть x > 0. Тогда 1 < x^y эквивалентно (1 < x и 0 < y) или (x < 1 и y < 0).

LaTeX

$$$ x > 0 \Rightarrow 1 < x^y \iff (1 < x \land 0 < y) \lor (x < 1 \land y < 0) $$$

Lean4

theorem one_lt_rpow_iff_of_pos (hx : 0 < x) : 1 < x ^ y ↔ 1 < x ∧ 0 < y ∨ x < 1 ∧ y < 0 := by
  rw [rpow_def_of_pos hx, one_lt_exp_iff, mul_pos_iff, log_pos_iff hx.le, log_neg_iff hx]

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