English
IsInitSeg(𝒜, r) holds when the collection of Finsets 𝒜 consists exactly of r many Finsets and is downward closed with respect to the colex order among Finsets of size r.
Русский
IsInitSeg(𝒜, r) означает, что 𝒜 состоит ровно из r конечных множеств и замкнуто снизу по колексному порядку среди множеств размером r.
LaTeX
$$$IsInitSeg(\mathcal{A}, r) \iff (\mathcal{A} : Set(\Finset(\alpha))).Sized(r) \wedge \\ \forall s,t.\; s \in \mathcal{A} \Rightarrow (toColex t < toColex s \land |t|=r) \Rightarrow t \in \mathcal{A}$$$
Lean4
/-- `𝒜` is an initial segment of the colexigraphic 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`. -/
def IsInitSeg (𝒜 : Finset (Finset α)) (r : ℕ) : Prop :=
(𝒜 : Set (Finset α)).Sized r ∧ ∀ ⦃s t : Finset α⦄, s ∈ 𝒜 → toColex t < toColex s ∧ #t = r → t ∈ 𝒜
