English
If s is dense in M and f: M → N is given together with a rule for products where the second factor lies in s, then there is a semigroup homomorphism extending f that respects those product rules.
Русский
Если s плотно в M и дано отображение f: M → N совместно с правилом для произведения x*y, когда y ∈ s, то существует гомоморфизм полугрупп, расширяющий f и удовлетворяющий этим правилам.
LaTeX
$$$\\text{ofDense}(f, hs, hmul): M \\to\\!\\! N$,\\; \\text{ где } hs: \\mathrm{closure}(s) = \\top, \\; hmul: \\forall x, \\forall y \\in s, f(xy) = f(x)f(y)$$$
Lean4
/-- Let `s` be a subset of a semigroup `M` such that the closure of `s` is the whole semigroup.
Then `MulHom.ofDense` defines a mul homomorphism from `M` asking for a proof
of `f (x * y) = f x * f y` only for `y ∈ s`. -/
@[to_additive]
def ofDense {M N} [Semigroup M] [Semigroup N] {s : Set M} (f : M → N) (hs : closure s = ⊤)
(hmul : ∀ (x), ∀ y ∈ s, f (x * y) = f x * f y) : M →ₙ* N
where
toFun := f
map_mul' x
y := dense_induction _ hs (fun y hy x => hmul x y hy) (fun y₁ y₂ h₁ h₂ x => by simp only [← mul_assoc, h₁, h₂]) y x
