card_div_mul_le_card_div_mul_card_mul

English

Let A,B,C be finite subsets of a 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**. Div-div-mul version. -/
@[to_additive /-- **Ruzsa's triangle inequality**. Sub-sub-add version. -/
    ]
theorem card_div_mul_le_card_div_mul_card_mul (A B C : Finset G) : #(A / C) * #B ≤ #(A / B) * #(B * C) :=
  by
  rw [← div_inv_eq_mul, div_eq_mul_inv]
  exact
    ruzsa_triangle_inequality_mul_div_div _ _
      _
        -- Auxiliary lemma towards the Plünnecke-Ruzsa inequality

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