IsMaxChain.range_fin_of_covBy

theorem IsMaxChain.range_fin_of_covBy : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : BoundedOrder α] {n : ℕ} {f : Fin (n + 1) → α}, f 0 = ⊥ → f (Fin.last n) = ⊤ → (∀ (k : Fin n), f k.castSucc ⩿ f k.succ) → IsMaxChain (fun x x_1 => x ≤ x_1) (Set.range f)

The theorem `IsMaxChain.range_fin_of_covBy` states that for any function `f : Fin (n + 1) → α`, where `α` is a type with a partial order and a bounded order, and `n` is a natural number, if the function `f` forms a tuple `(f₀, …, fₙ)` such that `f₀` is the least element `⊥` and `fₙ` is the greatest element `⊤`, and for all `0 ≤ k < n`, `fₖ₊₁` weakly covers `fₖ` (meaning `fₖ ≤ fₖ₊₁` and there is no `c` such that `fₖ

More concisely: If `f : Fin (n + 1) → α` is a function with `α` being a type with a partial order and a bounded order, such that `f` forms a tuple `(f₀, …, fₙ)` with `f₀ = ⊥`, `fₙ = ⊤`, and `fₖ ≤ fₖ₊₁` for all `0 ≤ k < n` with no strict in-between elements, then the range of `f` forms a maximal chain.