instBot — Mathlib

English

There is a bottom sublattice: the smallest sublattice whose carrier is the empty set, with closure properties of ∅.

Русский

Существует нижняя подрешетка: наименьшая подрешетка с носителем пустого множества.

LaTeX

$$$ Bot\\,(Sublattice\\,\\alpha) $$$

Lean4

/-- The empty sublattice of a lattice. -/
instance instBot : Bot (Sublattice α) where
  bot.carrier := ∅
  bot.supClosed' := supClosed_empty
  bot.infClosed' := infClosed_empty

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