English
If a net of homomorphisms from M1 to M2 converges pointwise to f, then there is a bundled monoid homomorphism M1 →* M2 whose underlying function is f.
Русский
Если сетка гомоморфизм M1 → M2 сходится по точкам к f, то существует связанный моноид-гомоморфизм M1 →* M2 с основанием f.
LaTeX
$$mulHomOfTendsto (f : M1 → M2) (g : α → F) [l.NeBot] (h : Tendsto (fun a x => g a x) l (nhds f)) : M1 →* M2$$
Lean4
/-- Construct a bundled semigroup homomorphism from a pointwise limit of semigroup homomorphisms. -/
@[to_additive (attr := simps! -fullyApplied) /--
Construct a bundled additive semigroup homomorphism from a pointwise limit of additive
semigroup homomorphisms -/
]
def mulHomOfTendsto (f : M₁ → M₂) (g : α → F) [l.NeBot] (h : Tendsto (fun a x => g a x) l (𝓝 f)) : M₁ →ₙ* M₂ :=
mulHomOfMemClosureRangeCoe f <| mem_closure_of_tendsto h <| Eventually.of_forall fun _ => mem_range_self _
