English
If g is an inducing map, then for any L and f, Multipliable f L holds exactly when Multipliable (g ∘ f) L holds and the L-indexed product ∏'[L] i, g(f i) lies in the image Range(g).
Русский
Если g индуктивно отображает топологическое пространство, тогда для любого L и f выражение о существовании бесконечного произведения сохраняется: Multipliable f L тогда и только тогда, когда Multipliable (g ∘ f) L и произведение ∏'[L] i, g(f(i)) принадлежит образу g.
LaTeX
$$Multipliable f L ↔ Multipliable (g ∘ f) L ∧ ∏'[L] i, g (f i) ∈ Set.range g$$
Lean4
@[to_additive]
theorem multipliable_iff_tprod_comp_mem_range [CommMonoid γ] [TopologicalSpace γ] [T2Space γ] {G} [FunLike G α γ]
[MonoidHomClass G α γ] {g : G} (hg : IsInducing g) (f : β → α) :
Multipliable f L ↔ Multipliable (g ∘ f) L ∧ ∏'[L] i, g (f i) ∈ Set.range g :=
by
constructor
· intro hf
constructor
· exact hf.map g hg.continuous
· by_cases hL : L.NeBot
· exact ⟨_, hf.map_tprod g hg.continuous⟩
· by_cases hfs : (mulSupport fun x ↦ g (f x)).Finite
· simp [tprod_bot hL, finprod_eq_prod, hfs, ← map_prod]
· exact ⟨1, by simp [tprod_bot hL, finprod_of_infinite_mulSupport hfs]⟩
· rintro ⟨hgf, a, ha⟩
use a
have := hgf.hasProd
simp_rw [comp_apply, ← ha] at this
exact (hg.hasProd_iff f a).mp this
