English
From a function f that lies in the closure of the range of a type F into M1 → M2, one can construct a bundled multiplicative homomorphism M1 →* M2 whose underlying function is f.
Русский
Из функции f, лежащей в замыкании образа отображения типа F в M1 → M2, строится связанный мультигомоморфизм M1 →* M2 с основанием f.
LaTeX
$$def mulHomOfMemClosureRangeCoe (f : M1 → M2) (hf : f ∈ closure (range fun (f : F) (x : M1) => f x)) : M1 →ₙ* M2$$
Lean4
/-- Construct a bundled semigroup 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 `MulHomClass` instance) to `M₁ → M₂`. -/
@[to_additive (attr := simps -fullyApplied) /--
Construct a bundled additive semigroup 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 `AddHomClass` instance) to `M₁ → M₂`. -/
]
def mulHomOfMemClosureRangeCoe (f : M₁ → M₂) (hf : f ∈ closure (range fun (f : F) (x : M₁) => f x)) : M₁ →ₙ* M₂
where
toFun := f
map_mul' := (isClosed_setOf_map_mul M₁ M₂).closure_subset_iff.2 (range_subset_iff.2 map_mul) hf
