rpow_lt_one_iff — Mathlib

English

For x ≥ 0, x^y < 1 holds iff x = 0 and y ≠ 0 or 1 < x and y < 0 or x < 1 and 0 < y.

Русский

Для x ≥ 0 верно: x^y < 1 тогда и только тогда, когда x = 0 и y ≠ 0, или 1 < x и y < 0, или x < 1 и 0 < y.

LaTeX

$$$ x \ge 0 \Rightarrow x^y < 1 \iff (x=0 \land y\neq 0) \lor (1 < x \land y < 0) \lor (x < 1 \land 0 < y) $$$

Lean4

theorem rpow_lt_one_iff (hx : 0 ≤ x) : x ^ y < 1 ↔ x = 0 ∧ y ≠ 0 ∨ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y :=
  by
  rcases hx.eq_or_lt with (rfl | hx)
  · rcases _root_.em (y = 0) with (rfl | hy) <;> simp [*, zero_lt_one]
  · simp [rpow_lt_one_iff_of_pos hx, hx.ne.symm]

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