ruzsa_triangle_inequality_mul_div_div

English

Let A, B, C be finite subsets of a commutative group G. Then |A/C| · |B| ≤ |A B| · |B/C|.

Русский

Пусть A, B, C — конечные подмножества коммутативной группы G. Тогда |A/C| · |B| ≤ |A B| · |B/C|.

LaTeX

$$$|A/C|\,|B| \le |A B|\,|B/C|$$$

Lean4

/-- **Ruzsa's triangle inequality**. Mul-div-div version. -/
@[to_additive /-- **Ruzsa's triangle inequality**. Add-sub-sub version. -/
    ]
theorem ruzsa_triangle_inequality_mul_div_div (A B C : Finset G) : #(A * C) * #B ≤ #(A / B) * #(B / C) :=
  by
  rw [div_eq_mul_inv, ← card_inv B, ← card_inv (B / C), inv_div', div_inv_eq_mul]
  exact ruzsa_triangle_inequality_mul_mul_mul _ _ _

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