eqOn_closure — Mathlib

English

If two multiplicative homomorphisms agree on a subset s, then they agree on the closure of s.

Русский

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

LaTeX

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

Lean4

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

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