English
The relation MonovaryOrder f g induces a strict total order on ι; i.e., on the index set there is a lexicographic-type order defined by f and g which is strict and total.
Русский
Отношение MonovaryOrder f g индуцирует строгий полный порядок на ι; то есть на множестве индексов существует лексикографоподобный порядок, задаваемый f и g, который строг и тотален.
LaTeX
$$$\text{IsStrictTotalOrder } ι\ (\mathrm{MonovaryOrder}(f,g))$$$
Lean4
instance : IsStrictTotalOrder ι (MonovaryOrder f g)
where
trichotomous i
j := by
convert trichotomous_of (Prod.Lex (· < ·) <| Prod.Lex (· < ·) WellOrderingRel) _ _
· simp only [Prod.ext_iff, ← and_assoc, imp_and, iff_and_self]
exact ⟨congr_arg _, congr_arg _⟩
· infer_instance
irrefl i := by rw [MonovaryOrder]; exact irrefl _
trans i j k := by rw [MonovaryOrder]; exact _root_.trans
