instLattice — Mathlib

English

There is a lattice structure on Subobject B for any B in C, given HasPullbacks, HasImages, HasBinaryCoproducts.

Русский

Для любого B в C существует решетка на Subobject(B), если в наличии имеется произведения типа pullback, изображения и копроизведения.

LaTeX

$$$\mathrm{Lattice}(\mathrm{Subobject}\, B)$$$

Lean4

instance {B : C} : Lattice (Subobject B) :=
  { Subobject.semilatticeInf, Subobject.semilatticeSup with }

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