English
The product over a sum index S ⊕ T of a family of topological modules is canonically isomorphic (both as a topological module and as a module) to the product of the product over S and the product over T.
Русский
Произведение по сумме индексов S ⊕ T из семейства топологических модулей изоморфно произведению по S и по T как в топологическом модуле, так и в модуле.
LaTeX
$$$\\big((st : S \\oplus T) \\to A\\,st\\big) \\cong_L[R] (\\{s : S \\to A(\\text{Sum.inl } s)\\}) \\times (\\{t : T \\to A(\\text{Sum.inr } t)\\})$$$
Lean4
/-- The product over `S ⊕ T` of a family of topological modules
is isomorphic (topologically and algebraically) to the product of
(the product over `S`) and (the product over `T`).
This is `Equiv.sumPiEquivProdPi` as a `ContinuousLinearEquiv`.
-/
def sumPiEquivProdPi (R : Type*) [Semiring R] (S T : Type*) (A : S ⊕ T → Type*) [∀ st, AddCommMonoid (A st)]
[∀ st, Module R (A st)] [∀ st, TopologicalSpace (A st)] :
((st : S ⊕ T) → A st) ≃L[R] ((s : S) → A (Sum.inl s)) × ((t : T) → A (Sum.inr t))
where
__ := LinearEquiv.sumPiEquivProdPi R S T A
__ := Homeomorph.sumPiEquivProdPi S T A
