preorder — Mathlib

English

If α is a preorder, then WithBot α is a preorder.

Русский

Если α задаёт опорный порядок, то WithBot α также задаёт порядок.

LaTeX

$$$\text{Preorder } \alpha \Rightarrow \text{Preorder }(\mathrm{WithBot}\,\alpha)$$$

Lean4

instance preorder [Preorder α] : Preorder (WithBot α)
    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

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