English
The binary product of Sublattices L ⊆ α and M ⊆ β is the Sublattice of α × β consisting of pairs (a,b) with a ∈ L and b ∈ M, with componentwise join and meet.
Русский
Двоичное произведение подрешёток L ⊆ α и M ⊆ β есть подрешётка α × β, содержащая пары (a,b) с a ∈ L, b ∈ M, со скобками по компонентам для операций сопоставления и частично-упорядочивания.
LaTeX
$$Sublattice.prod L M : Sublattice (α × β)$$
Lean4
/-- Binary product of sublattices as a sublattice. -/
@[simps]
def prod (L : Sublattice α) (M : Sublattice β) : Sublattice (α × β)
where
carrier := L ×ˢ M
supClosed' := L.supClosed.prod M.supClosed
infClosed' := L.infClosed.prod M.infClosed
