Theorems · Theorem · combinatorics

Finset.card_div_choose_le_card_shadow_div_choose

∀ {𝕜 : Type u_1} {α : Type u_2} [inst : Semifield 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : DecidableEq α] [inst_4 : Fintype α] {𝒜 : Finset (Finset α)} {r : ℕ},
  r ≠ 0 → Set.Sized r ↑𝒜 → ↑𝒜.card / ↑((Fintype.card α).choose r) ≤ ↑𝒜.shadow.card / ↑((Fintype.card α).choose (r - 1))

The downward local LYM inequality. 𝒜 takes up less of α^(r) (the finsets of card r) than ∂𝒜 takes up of α^(r - 1).

Defined in

Mathlib.Combinatorics.SetFamily.LYM

Cited by

0 results in Mathlib

Foundations

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

Assumes

SemifieldLinearOrderIsStrictOrderedRingDecidableEqFintype