pow_lt_one_iff — Mathlib

English

For n > 0, x^n < 1 iff x < 1, under right-strict-mono.

Русский

Для n > 0 верно: x^n < 1 ⇔ x < 1, при правой строгой монотонности.

LaTeX

$$$(0 < n) \Rightarrow (x^n < 1 \iff x < 1)$$$

Lean4

@[to_additive]
theorem pow_lt_one_iff [MulRightStrictMono M] {n : ℕ} {x : M} (hn : 0 < n) : x ^ n < 1 ↔ x < 1 :=
  haveI := mulRightMono_of_mulRightStrictMono M
  ⟨fun H => not_le.mp fun k => H.not_ge <| Right.one_le_pow_of_le k, Right.pow_lt_one_of_lt hn⟩

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