preorder — Mathlib

English

There is a natural preorder on WithTop(α) extending the preorder of α.

Русский

Существует естественный предпорядок на WithTop(α), расширяющий предпорядок α.

LaTeX

$$$$ \\text{Preorder}(\\mathrm{WithTop}(\\alpha)). $$$$

Lean4

instance preorder [Preorder α] : Preorder (WithTop α)
    where
  lt_iff_le_not_ge x y := by cases x <;> cases y <;> simp [lt_iff_le_not_ge]
  le_refl x := by cases x <;> simp [le_def]
  le_trans x y z := by cases x <;> cases y <;> cases z <;> simp [le_def]; simpa using le_trans

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