Theorems · Theorem · combinatorics

Finset.le_card_falling_div_choose

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

A bound on any top part of the sum in LYM in terms of the size of falling k 𝒜.

Defined in

Mathlib.Combinatorics.SetFamily.LYM

Cited by

1 results in Mathlib

Foundations

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

Assumes

SemifieldLinearOrderIsStrictOrderedRingDecidableEqFintype