eqOn_closure — Mathlib

English

If two monoid homomorphisms agree on a set s, they agree on the subgroup closure of s.

Русский

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

LaTeX

$$$\mathrm{EqOn}(f,g;s) \Rightarrow \mathrm{EqOn}(f,g;\mathrm{closure}(s))$$$

Lean4

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

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