Products of vector lattices #
The pointwise product of vector lattices is a vector lattice. This is the product
instance from BanLat Pi.lean; the separate finite-dimensional normed products
are outside the dependency closure of the order-adherence constructions.
Pointwise product #
@[instance_reducible]
instance
Pi.instVectorLattice
{ι : Type u_1}
{X : ι → Type u_2}
[(i : ι) → AddCommGroup (X i)]
[(i : ι) → Lattice (X i)]
[∀ (i : ι), IsOrderedAddMonoid (X i)]
[(i : ι) → VectorLattice (X i)]
:
VectorLattice ((i : ι) → X i)
The pointwise product of a family of vector lattices is a vector lattice.
The lattice operations and absolute value are computed pointwise (see
Pi.sup_apply, Pi.inf_apply, Pi.abs_apply in Mathlib).