lt_inv_smul_iff_of_pos — Mathlib

English

For a > 0 and SMulPosStrictMono, b1 < a⁻¹ • b2 is equivalent to a • b1 < b2.

Русский

Для a > 0 и SMulPosStrictMono, b1 < a⁻¹ • b2 эквивалентно a • b1 < b2.

LaTeX

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

Lean4

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

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