le_card_inter_finset — Mathlib

English

A Harris–Kleitman bound for two lower sets of Finsets: a quantitative relation between their sizes and the size of their intersection.

Русский

Гаррис–Клейтман для двух нижних множеств множест: численное соотношение их размеров и размера пересечения.

LaTeX

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

Lean4

/-- **Harris-Kleitman inequality**: Any two lower sets of finsets correlate. -/
theorem le_card_inter_finset (h𝒜 : IsLowerSet (𝒜 : Set (Finset α))) (hℬ : IsLowerSet (ℬ : Set (Finset α))) :
    #𝒜 * #ℬ ≤ 2 ^ Fintype.card α * #(𝒜 ∩ ℬ) :=
  h𝒜.le_card_inter_finset' hℬ (fun _ _ => subset_univ _) fun _ _ => subset_univ _

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