instCompletelyDistribLattice — Mathlib

English

If α and β are completely distributive lattices, then α × β is a completely distributive lattice.

Русский

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

LaTeX

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

Lean4

instance instCompletelyDistribLattice [CompletelyDistribLattice α] [CompletelyDistribLattice β] :
    CompletelyDistribLattice (α × β) where
  __ := instFrame
  __ := instCoframe
  iInf_iSup_eq f := by ext <;> simp [fst_iSup, fst_iInf, snd_iSup, snd_iInf, iInf_iSup_eq]

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