one_lt_oneLePart — Mathlib

English

If ha: 1 < a, then 1 < a⁻ᵐ; i.e., a strictly greater than 1 implies its negative part is strictly greater than 1.

Русский

Если ha: 1 < a, то 1 < a⁻ᵐ; иначе говоря, больше единицы в исходном элементе влечёт увеличение части отрицательной.

LaTeX

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

Lean4

@[to_additive (attr := simp) posPart_pos]
theorem one_lt_oneLePart (ha : 1 < a) : 1 < a⁺ᵐ := by rwa [oneLePart_eq_self.2 ha.le]

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