English
The map M ↦ L.prod M is monotone in M.
Русский
Отображение M ↦ L.prod M монотонно по M.
LaTeX
$$Monotone(M \\mapsto L \\prod M)$$
Lean4
/-- Arbitrary product of sublattices. Given an index set `s` and a family of sublattices
`L : Π i, Sublattice (α i)`, `pi s L` is the sublattice of dependent functions `f : Π i, α i` such
that `f i` belongs to `L i` whenever `i ∈ s`. -/
@[simps]
def pi (s : Set κ) (L : ∀ i, Sublattice (π i)) : Sublattice (∀ i, π i)
where
carrier := s.pi fun i ↦ L i
supClosed' := supClosed_pi fun i _ ↦ (L i).supClosed
infClosed' := infClosed_pi fun i _ ↦ (L i).infClosed
