toLattice — Mathlib

English

Every linear order can be endowed with a lattice structure by defining join as maximum and meet as minimum.

Русский

Каждый линейный порядок можно наделить структурой решётки, определив объединение как максимум и пересечение как минимум.

LaTeX

$$$\forall a,b:\alpha,\ a \vee b = \max(a,b) \land a \wedge b = \min(a,b)$$$

Lean4

instance (priority := 100) toLattice {α : Type u} [LinearOrder α] : Lattice α
    where
  sup := max
  inf := min
  le_sup_left := le_max_left; le_sup_right := le_max_right; sup_le _ _ _ := max_le
  inf_le_left := min_le_left; inf_le_right := min_le_right; le_inf _ _ _ := le_min

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