instPreorder — Mathlib

English

WithZero α is equipped with a preorder extending that of α, defined by lt_iff_le_not_ge (and compatible le).

Русский

WithZero α оснащён предорядком, который расширяет предорядок α и определяется через lt_iff_le_not_ge (и совместим с ≤).

LaTeX

$$$ x < y \iff \exists b : α, y = \uparrow b \land \forall a : α, x = \uparrow a \rightarrow a < b \;\land\; x \le y \text{ defined compatibly} $$$

Lean4

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

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