instSubsingletonPredOrder — Mathlib

English

There is at most one PredOrder structure on a given PartialOrder.

Русский

Существует не более одной структуры PredOrder на заданном PartialOrder.

LaTeX

$$$ \\text{Subsingleton} (\\mathrm{PredOrder}\\ \\alpha)$$$

Lean4

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

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