instLattice — Mathlib

English

If each α'(i) carries a lattice structure, then the function space ∀i, α'(i) carries a lattice structure pointwise.

Русский

Если каждая α'(i) обладает структурой решетки, то пространство функций ∀i, α'(i) обладает структурой решетки по точечной схеме.

LaTeX

$$$ \forall i,\, \text{Lattice}(\alpha'(i)) \Rightarrow \text{Lattice}(\forall i,\alpha'(i)) $$$

Lean4

instance instLattice [∀ i, Lattice (α' i)] : Lattice (∀ i, α' i) where

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