top_def — Mathlib

English

Let α be a type. The top element of the lattice of equivalence relations on α is the indiscrete (universal) relation, where every pair of elements is related. Equivalently, the underlying comparison function is constantly true.

Русский

Пусть α — тип. Верхний элемент решетки отношений эквивалентности на α — универcальное отношение, в котором любые две элементы эквивалентны. Эквивалентно: соответствующая функция всегда истинна.

LaTeX

$$$$ \\forall x,y:\\alpha,\\ x \\sim y \\text{ (with respect to the top relation)}. $$$$

Lean4

@[simp]
theorem top_def : ⇑(⊤ : Setoid α) = ⊤ :=
  rfl

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