English
Given a bounded poset α, a function f: Fin(n+1) → α with f(0) = ⊥, f(last n) = ⊤, and f(k.castSucc) ⩿ f(k.succ) for all k < n, the range of f forms a Flag α.
Русский
Пусть α — ограниченная частично упорядоченная множество, f: Fin(n+1) → α удовлетворяет f(0) = ⊥, f(last n) = ⊤ и f(k.castSucc) ⩿ f(k.succ) для всех k < n; тогда множество значений f образует флаг в α.
LaTeX
$$$\\forall f: \\mathrm{Fin}(n+1) \\to \\alpha,\\; f(0)=\\bot \\land f(\\mathrm{last}\\,n)=\\top \\land \\forall k: \\mathrm{Fin}\,n,\\; f(k.castSucc) \\operatorname{covBy} f(k.succ) \\Rightarrow \\operatorname{range}(f) \\in \\operatorname{Flag}(\\alpha)$$$$
Lean4
/-- Let `f : Fin (n + 1) → α` be an `(n + 1)`-tuple `(f₀, …, fₙ)` such that
- `f₀ = ⊥` and `fₙ = ⊤`;
- `fₖ₊₁` weakly covers `fₖ` for all `0 ≤ k < n`;
this means that `fₖ ≤ fₖ₊₁` and there is no `c` such that `fₖ<c<fₖ₊₁`.
Then the range of `f` is a `Flag α`. -/
@[simps]
def rangeFin (f : Fin (n + 1) → α) (h0 : f 0 = ⊥) (hlast : f (.last n) = ⊤)
(hcovBy : ∀ k : Fin n, f k.castSucc ⩿ f k.succ) : Flag α
where
carrier := range f
Chain' := (IsMaxChain.range_fin_of_covBy h0 hlast hcovBy).1
max_chain' := (IsMaxChain.range_fin_of_covBy h0 hlast hcovBy).2
