ofUnique — Mathlib

English

If γ is a preorder with a unique element, then FiniteDimensionalOrder γ holds.

Русский

Если γ — множество с предикатом порядка и единственным элементом, то FiniteDimensionalOrder γ верно.

LaTeX

$$$$ \\text{FiniteDimensionalOrder}(\\gamma) \\text{ holds when } \\gamma \\text{ is unique under } \\le. $$$$

Lean4

instance ofUnique (γ : Type*) [Preorder γ] [Unique γ] : FiniteDimensionalOrder γ where
  exists_longest_relSeries :=
    ⟨.singleton _ default, fun x ↦ by
      by_contra! r
      exact (x.step ⟨0, by omega⟩).ne <| Subsingleton.elim _ _⟩

Похожие утверждения