Theorems · Definition · combinatorics

Finset.Colex.IsInitSeg

{α : Type u_1} → [LinearOrder α] → Finset (Finset α) → ℕ → Prop

𝒜 is an initial segment of the colexicographic order on sets of r, and that if t is below s in colex where t has size r and s is in 𝒜, then t is also in 𝒜. In effect, 𝒜 is downwards closed with respect to colex among sets of size r.

Defined in

Mathlib.Combinatorics.Colex

Cited by

9 results in Mathlib

Foundations

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

Assumes

LinearOrder