English
Flattened pi construction maps a family of continuous multilinear maps into a single multilinear map into a product space.
Русский
Свернуть конструкцию pi в единое мультиляйн отображение в произведение пространств.
LaTeX
$$$\\pi: (i \\mapsto CMM) \\to CMM$$$
Lean4
/-- Combine a family of continuous multilinear maps with the same domain and codomains `M' i` into a
continuous multilinear map taking values in the space of functions `∀ i, M' i`. -/
def pi {ι' : Type*} {M' : ι' → Type*} [∀ i, AddCommMonoid (M' i)] [∀ i, TopologicalSpace (M' i)] [∀ i, Module R (M' i)]
(f : ∀ i, ContinuousMultilinearMap R M₁ (M' i)) : ContinuousMultilinearMap R M₁ (∀ i, M' i)
where
cont := continuous_pi fun i => (f i).coe_continuous
toMultilinearMap := MultilinearMap.pi fun i => (f i).toMultilinearMap
