card_inter_le_finset — Mathlib

English

Another variant of the Harris–Kleitman bounds for lower/upper set interactions via intersections and unions.

Русский

Еще одно вариационное неравенство Харриса–Клейтмана для взаимодействия нижних и верхних множеств через пересечения и объединения.

LaTeX

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

Lean4

/-- **Harris-Kleitman inequality**: Lower sets and upper sets of finsets anticorrelate. -/
theorem card_inter_le_finset (h𝒜 : IsLowerSet (𝒜 : Set (Finset α))) (hℬ : IsUpperSet (ℬ : Set (Finset α))) :
    2 ^ Fintype.card α * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ :=
  by
  rw [inter_comm, mul_comm #𝒜]
  exact hℬ.card_inter_le_finset h𝒜

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