instCompleteDistribLattice — Mathlib

English

If α and β are complete distributive lattices, then their product α × β is a complete distributive lattice.

Русский

Если α и β являются полными распределимыми решётками, то их произведение α × β также является полной распределимой решёткой.

LaTeX

$$$[CompleteDistribLattice\; \alpha] \land [CompleteDistribLattice\; \beta] \Rightarrow CompleteDistribLattice(\alpha \times \beta).$$$

Lean4

instance instCompleteDistribLattice [CompleteDistribLattice β] : CompleteDistribLattice (α × β)
    where
  __ := instFrame
  __ := instCoframe

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