instSubsingletonSuccOrder — Mathlib

English

In any partially ordered set, the successor structure on α is unique: there is at most one way to define the successor relation making α a SuccOrder.

Русский

Для частично упорядоченного множества существует не более одной структуры SuccOrder, то есть операция перехода к следующему уникальна.

LaTeX

$$$ \forall s_1,s_2 : \mathrm{SuccOrder}(\alpha),\ s_1 = s_2 $$$

Lean4

/-- There is at most one way to define the successors in a `PartialOrder`. -/
instance [PartialOrder α] : Subsingleton (SuccOrder α) :=
  ⟨by
    intro h₀ h₁
    ext a
    by_cases ha : IsMax a
    · exact (@IsMax.succ_eq _ _ h₀ _ ha).trans ha.succ_eq.symm
    · exact @CovBy.succ_eq _ _ h₀ _ _ (covBy_succ_of_not_isMax ha)⟩

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