card_le_card_diffs — Mathlib

English

Special case of the Marica–Schonheim bound when comparing the total sizes of two subfamilies against their symmetric differences.

Русский

Специальный случай границы Марича–Шёнхайма для суммарных размеров подсемейств по отношению к их симметрическим различиям.

LaTeX

$$$$|\\mathcal{A}|\\cdot|\\mathcal{B}| \\le 2^{|\\alpha|}\\;|\\mathcal{A}\\cap\\mathcal{B}|$$$$

Lean4

/-- The **Marica-Schönheim Inequality**. -/
theorem card_le_card_diffs (s : Finset α) : #s ≤ #(s \\ s) :=
  le_of_pow_le_pow_left₀ two_ne_zero (zero_le _) <| by simpa [← sq] using s.le_card_diffs_mul_card_diffs s

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