lattice — Mathlib

English

A simple order with decidable equality yields a linear order; i.e., any two elements are comparable.

Русский

Простой порядок с разрешимым равенством даёт линейный порядок; любые два элемента сравнимы.

LaTeX

$$$\text{IsSimpleOrder.linearOrder} : LinearOrder α$$$

Lean4

/-- A simple partial ordered `BoundedOrder` induces a lattice.
This is not an instance to prevent loops -/
protected def lattice {α} [DecidableEq α] [PartialOrder α] [BoundedOrder α] [IsSimpleOrder α] : Lattice α :=
  @LinearOrder.toLattice α IsSimpleOrder.linearOrder

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