ruzsa_triangle_inequality_mulInv_mulInv_mulInv

English

Ruzsa's triangle inequality in div-inv form: #B · #(A⁻¹·C) ≤ #(B⁻¹·A) · #(B⁻¹·C).

Русский

Неравенство Рузa в форме деления и инверсии.

LaTeX

$$$#B \\cdot #(A^{-1} \\cdot C) \\leq #(B^{-1} \\cdot A) \\cdot #(B^{-1} \\cdot C)$$$

Lean4

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

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