English
If g has a left inverse g' with g' and g continuous, then for any L-multipliable family f, the image under g of the L-indexed product equals the L-indexed product of the images, i.e., g(∏'[L] b, f(b)) = ∏'[L] b, g(f(b)).
Русский
Если у отображения g есть левая обратная g' (обратная слева) и обе непрерывны, то для любой семейства f, определённого через индекс L, образ через g сохраняет произведение: g(∏'[L] b, f(b)) = ∏'[L] b, g(f(b)).
LaTeX
$$$g\left(\prod'[L] b, f b\right) = \prod'[L] b, g(f b).$$$
Lean4
/-- Special case of `Topology.IsClosedEmbedding.map_tprod`, logically weaker but possibly easier
to apply in practice. -/
@[to_additive /-- Special case of `Topology.IsClosedEmbedding.map_tsum`, logically weaker but
possibly easier to apply in practice. -/
]
theorem map_tprod {G : Type*} (f : β → α) [CommMonoid γ] [TopologicalSpace γ] [T2Space γ] {g : G} [FunLike G α γ]
[MonoidHomClass G α γ] (hg : Continuous g) {g' : γ → α} (hg' : Continuous g') (hgg' : LeftInverse g' g) :
g (∏'[L] b, f b) = ∏'[L] b, g (f b) :=
(hgg'.isClosedEmbedding hg' hg).map_tprod _
