instTop — Mathlib

English

There is a top sublattice: the largest sublattice whose carrier is the whole lattice α, with closure properties of univ.

Русский

Существуют верхняя подрешетка, содержащая все элементы решетки.

LaTeX

$$$ Top\\,(Sublattice\\,\\alpha) $$$

Lean4

/-- The maximum sublattice of a lattice. -/
instance instTop : Top (Sublattice α) where
  top.carrier := univ
  top.supClosed' := supClosed_univ
  top.infClosed' := infClosed_univ

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