one_lt_ltOnePart_iff — Mathlib

English

For all a, the equivalence 1 < a⁻ᵐ ↔ a < 1 holds in a linear ordered group with left-monotone multiplication.

Русский

Для любого a в линейно упорядоченной группе с левосторонней монотонностью умножения верна эквивалентность 1 < a⁻ᵐ ↔ a < 1.

LaTeX

$$1 < a^{-m} \iff a < 1$$

Lean4

@[to_additive (attr := simp) negPart_pos_iff]
theorem one_lt_ltOnePart_iff : 1 < a⁻ᵐ ↔ a < 1 :=
  lt_iff_lt_of_le_iff_le <| (one_le_leOnePart _).ge_iff_eq'.trans leOnePart_eq_one

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