English
From a function f in the closure of the range of the coercion from F to M1 → M2, construct a bundled monoid homomorphism M1 →* M2 with toFun = f.
Русский
Из f, лежащей в замыкании образа включения F → M1 → M2, строится связанный моноид-гомоморфизм M1 →* M2 с toFun=f.
LaTeX
$$def monoidHomOfMemClosureRangeCoe (f : M1 → M2) (hf : f ∈ closure (range fun (f : F) (x : M1) => f x)) : M1 →* M2$$
Lean4
/-- Construct a bundled monoid homomorphism `M₁ →* M₂` from a function `f` and a proof that it
belongs to the closure of the range of the coercion from `M₁ →* M₂` (or another type of bundled
homomorphisms that has a `MonoidHomClass` instance) to `M₁ → M₂`. -/
@[to_additive (attr := simps -fullyApplied) /--
Construct a bundled additive monoid homomorphism `M₁ →+ M₂` from a function `f`
and a proof that it belongs to the closure of the range of the coercion from `M₁ →+ M₂` (or another
type of bundled homomorphisms that has an `AddMonoidHomClass` instance) to `M₁ → M₂`. -/
]
def monoidHomOfMemClosureRangeCoe (f : M₁ → M₂) (hf : f ∈ closure (range fun (f : F) (x : M₁) => f x)) : M₁ →* M₂
where
toFun := f
map_one' := (isClosed_setOf_map_one M₁ M₂).closure_subset_iff.2 (range_subset_iff.2 map_one) hf
map_mul' := (isClosed_setOf_map_mul M₁ M₂).closure_subset_iff.2 (range_subset_iff.2 map_mul) hf
