inv_smul_le_iff_of_pos — Mathlib

English

For a > 0 in a GroupWithZero acting on β with the PosSMulMono property, we have a smul-inequality translation relating a, b1, b2: a⁻¹ • b1 ≤ b2 iff b1 ≤ a • b2.

Русский

Для a > 0 в группе с нулём, действующей на β при PosSMulMono, имеем эквивалентность: a⁻¹ • b1 ≤ b2 iff b1 ≤ a • b2.

LaTeX

$$$[GroupWithZero α] \;[Preorder α][Preorder β] \\;\\Rightarrow\\; (a>0) \\Rightarrow (a^{-1} \\cdot b_1 \\le b_2 \\Leftrightarrow b_1 \\le a \\cdot b_2)$$$

Lean4

theorem inv_smul_le_iff_of_pos [PosSMulMono α β] [PosSMulReflectLE α β] (ha : 0 < a) : a⁻¹ • b₁ ≤ b₂ ↔ b₁ ≤ a • b₂ := by
  rw [← smul_le_smul_iff_of_pos_left ha, smul_inv_smul₀ ha.ne']

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