English
Let g be a closed embedding between topological monoids. Then for any index set and 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] i, f(i)) = ∏'[L] i, g(f(i)).
Русский
Пусть g — замкнутое вложение между топологическими моноидами. Тогда для любой совокупности индексного множества и любой семьи f, умножение по индексу сохраняется под отображением g: g(∏'[L] i, f(i)) = ∏'[L] i, g(f(i)).
LaTeX
$$$g\left(\prod'[L] i, f i\right) = \prod'[L] i, g(f i).$$$
Lean4
@[to_additive]
theorem map_tprod {ι α α' G : Type*} [CommMonoid α] [CommMonoid α'] [TopologicalSpace α] [TopologicalSpace α']
[T2Space α'] (f : ι → α) {L : SummationFilter ι} {g : G} [FunLike G α α'] [MonoidHomClass G α α']
(hge : Topology.IsClosedEmbedding g) : g (∏'[L] i, f i) = ∏'[L] i, g (f i) :=
by
by_cases hL : L.NeBot
· by_cases h : Multipliable f L
· exact h.map_tprod g hge.continuous
· rw [tprod_eq_one_of_not_multipliable h, tprod_eq_one_of_not_multipliable, map_one]
contrapose! h
simp only [Multipliable, HasProd] at h ⊢
obtain ⟨b, hb⟩ := h
obtain ⟨a, ha⟩ : b ∈ Set.range g := hge.isClosed_range.mem_of_tendsto hb (.of_forall <| by simp [← map_prod])
use a
simp [hge.tendsto_nhds_iff, Function.comp_def, ha, hb]
· simpa [tprod_bot hL] using (MonoidHomClass.toMonoidHom g).map_finprod_of_injective hge.injective _
