Theorems · Theorem · combinatorics

Finset.Colex.shadow_initSeg

∀ {α : Type u_1} [inst : LinearOrder α] {s : Finset α} [inst_1 : Fintype α] (hs : s.Nonempty),
  (Finset.Colex.initSeg s).shadow = Finset.Colex.initSeg (s.erase (s.min' hs))

This is important for iterating Kruskal-Katona: the shadow of an initial segment is also an initial segment.

Defined in

Mathlib.Combinatorics.SetFamily.KruskalKatona

Cited by

1 results in Mathlib

Foundations

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

Assumes

LinearOrderFintype