ruzsa_triangle_inequality_mulInv_mul_mul

English

Alternative presentation of Ruzsa's triangle inequality in division-multiplication-multiplication form.

Русский

Альтернативная формулировка неравенства Рузы.

LaTeX

$$$ #(A/C) \\cdot \\#B \\leq \\#(A/B) \\cdot \\#(C/B) $$$

Lean4

/-- **Ruzsa's triangle inequality**. Mulinv-mul-mul version. -/
@[to_additive /-- **Ruzsa's triangle inequality**. Addneg-add-add version. -/
    ]
theorem ruzsa_triangle_inequality_mulInv_mul_mul (A B C : Finset G) : #(A * C⁻¹) * #B ≤ #(A * B) * #(C * B) := by
  simpa using ruzsa_triangle_inequality_mulInv_mulInv_mulInv A B⁻¹ C

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