instLattice — Mathlib

English

If β is a lattice, then Germ l β inherits a lattice structure, combining the semilatticeSup and semilatticeInf structures.

Русский

Если β является решёткой, то Germ l β наследует структуру решётки, объединяя верхнюю и нижнюю частичные структуры.

LaTeX

$$$\\text{Lattice}(\\mathrm{Germ}_l \\beta)$ obtained from $\\text{SemilatticeSup}$ and $\\text{SemilatticeInf}$$$

Lean4

instance instLattice [Lattice β] : Lattice (Germ l β)
    where
  __ := instSemilatticeSup
  __ := instSemilatticeInf

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