ruzsa_triangle_inequality_mul_mul_invMul

English

Let A, B, C be finite subsets of a group G. Then the product-set sizes satisfy |A C| · |B| ≤ |A B| · |C^{-1} B|.

Русский

Пусть A, B, C — конечные подмножества группы G. Тогда выполняется неравенство по размерам множеств: |A C| · |B| ≤ |A B| · |C^{-1} B|.

LaTeX

$$$|A C|\,|B| \le |A B|\,|C^{-1} B|$$$

Lean4

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

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