Theorems · Theorem · combinatorics

Finset.lubell_yamamoto_meshalkin_inequality_sum_card_div_choose

∀ {𝕜 : Type u_1} {α : Type u_2} [inst : Semifield 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : Fintype α] {𝒜 : Finset (Finset α)},
  IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜 →
    ∑ r ∈ Finset.range (Fintype.card α + 1), ↑(𝒜.slice r).card / ↑((Fintype.card α).choose r) ≤ 1

The Lubell-Yamamoto-Meshalkin inequality, also known as the LYM inequality. If 𝒜 is an antichain, then the sum of the proportion of elements it takes from each layer is less than 1.

Defined in

Mathlib.Combinatorics.SetFamily.LYM

Cited by

2 results in Mathlib

Foundations

Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemifieldLinearOrderIsStrictOrderedRingFintype