inv_smul_lt_iff_of_pos — Mathlib

English

If a > 0 and SMulPosMono holds, then a⁻¹ • b1 < b2 iff b1 < a • b2.

Русский

Если a > 0 и SMulPosMono, то a⁻¹ • b1 < b2 эквивалентно b1 < a • b2.

LaTeX

$$$[PosSMulStrictMono α β] \\Rightarrow (a>0) \\Rightarrow (a^{-1} \\cdot b_1 < b_2 \\iff b_1 < a \\cdot b_2)$$$

Lean4

theorem inv_smul_lt_iff_of_pos [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : 0 < a) :
    a⁻¹ • b₁ < b₂ ↔ b₁ < a • b₂ := by rw [← smul_lt_smul_iff_of_pos_left ha, smul_inv_smul₀ ha.ne']

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