eqOn_closureM — Mathlib

English

If two monoid homomorphisms f,g agree on a set s, they agree on its submonoid closure: eqOn_closureM.

Русский

Если две гомоморфизмы Моноида f,g совпадают на множестве s, они совпадают на замыкании подмонома: eqOn_closureM.

LaTeX

$$$\\text{eqOn}\\ f\\ g\\ s \\rightarrow \\text{EqOn}\\ f\\ g\\ (closure\\ s)$$$

Lean4

/-- If two monoid homomorphisms are equal on a set, then they are equal on its submonoid closure. -/
@[to_additive /-- If two monoid homomorphisms are equal on a set, then they are equal on its submonoid
      closure. -/
    ]
theorem eqOn_closureM {f g : M →* N} {s : Set M} (h : Set.EqOn f g s) : Set.EqOn f g (closure s) :=
  show closure s ≤ f.eqLocusM g from closure_le.2 h

Похожие утверждения