topEquiv — Mathlib

English

Let α be a lattice. The top sublattice ⊤ of α is order-isomorphic to α via the identity map (the carrier of ⊤ is univ).

Русский

Пусть α — решётка. Верхняя подрешетка ⊤ в α изоморфна по порядку самой α посредством тождественного отображения (каркас ⊤ равен универсума).

LaTeX

$$$(\top : \text{Sublattice } \alpha) \cong_o \alpha$$$

Lean4

/-- The top sublattice is isomorphic to the original lattice.

This is the sublattice version of `Equiv.Set.univ α`. -/
def topEquiv : (⊤ : Sublattice α) ≃o α where
  toEquiv := Equiv.Set.univ _
  map_rel_iff' := Iff.rfl

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