English
Let f: Fin(n+1) → α be an (n+1)-tuple with bottom and top two extremal elements and with successive terms covering the previous ones; then the range of f forms a maximal chain in α.
Русский
Пусть f: Fin(n+1) → α — последовательность длины n+1, начинающаяся с нижнего элемента и завершающаяся верхним, пары соседних элементов образуют каскад, тогда множество значений f образует максимальную цепь в α.
LaTeX
$$$\text{If } f: \mathrm{Fin}(n+1) \to \alpha ext{ satisfies } f(0)=\bot,\; f(\mathrm{last}\,n)=\top,\; f(k\text{.castSucc}) \lesssim f(k\text{.succ})\ (\forall k:\mathrm{Fin}\,n),\text{ then } \mathrm{range}(f) ext{ is a maximal chain in } \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 maximal chain. -/
theorem range_fin_of_covBy (h0 : f 0 = ⊥) (hlast : f (.last n) = ⊤) (hcovBy : ∀ k : Fin n, f k.castSucc ⩿ f k.succ) :
IsMaxChain (· ≤ ·) (range f) :=
by
have hmono : Monotone f := Fin.monotone_iff_le_succ.2 fun k ↦ (hcovBy k).1
refine ⟨hmono.isChain_range, fun t htc hbt ↦ hbt.antisymm fun x hx ↦ ?_⟩
rw [mem_range]; by_contra! h
suffices ∀ k, f k < x by simpa [hlast] using this (.last _)
intro k
induction k using Fin.induction with
| zero => simpa [h0, bot_lt_iff_ne_bot] using (h 0).symm
| succ k ihk =>
rw [range_subset_iff] at hbt
exact (htc.lt_of_le (hbt k.succ) hx (h _)).resolve_right ((hcovBy k).2 ihk)
