ruzsa_triangle_inequality_invMul_mul_mul

English

Ruzsa's triangle inequality in the mul-inv-mul-mul form: #(B.card) ≤ … (illustrative form).

Русский

Неравенство Рузы в форме умножение-инверсия‑умножение‑умножение.

LaTeX

$$$\\text{instLENat.le} (|B| \\cdot (|A|) , \\dots)$$$

Lean4

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

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