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