isWellOrder — Mathlib

English

On a subsingleton type, any irreflexive relation is a well-order.

Русский

На одноклеточном (единичном) типе любое иррефлексивное отношение является хорошо упорядоченным.

LaTeX

$$[Subsingleton α] (r : α → α → Prop) [IsIrrefl α r] : IsWellOrder α r$$

Lean4

theorem isWellOrder [Subsingleton α] (r : α → α → Prop) [hr : IsIrrefl α r] : IsWellOrder α r :=
  { hr with trichotomous := fun a b => Or.inr <| Or.inl <| Subsingleton.elim a b,
    trans := fun a b _ h => (not_rel_of_subsingleton r a b h).elim,
    wf := ⟨fun a => ⟨_, fun y h => (not_rel_of_subsingleton r y a h).elim⟩⟩ }

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