one_lt_rpow_iff — Mathlib

English

Let x ≥ 0 be a nonnegative real number and y be a real number. Then 1 < x^y if and only if either x > 1 and y > 0, or 0 < x < 1 and y < 0.

Русский

Пусть x ≥ 0 — неотрицательное вещественное число, и y — вещественное число. Тогда 1 < x^y эквивалентно либо x > 1 и y > 0, либо 0 < x < 1 и y < 0.

LaTeX

$$$1 < x^{y} \iff (1 < x \land 0 < y) \lor (0 < x \land x < 1 \land y < 0)$$$

Lean4

theorem one_lt_rpow_iff (hx : 0 ≤ x) : 1 < x ^ y ↔ 1 < x ∧ 0 < y ∨ 0 < x ∧ x < 1 ∧ y < 0 :=
  by
  rcases hx.eq_or_lt with (rfl | hx)
  · rcases _root_.em (y = 0) with (rfl | hy) <;> simp [*, (zero_lt_one' ℝ).not_gt]
  · simp [one_lt_rpow_iff_of_pos hx, hx]

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