eq_of_eqOn_set_dense — Mathlib

English

If two nonunital ring homomorphisms f,g agree on a dense subset s of R (i.e., closure(s) = ⊤), then f = g.

Русский

Если два гомоморфизма f,g: R →ₙ+* S совпадают на плотном подмножестве s (замыкание s = ⊤), то f = g.

LaTeX

$$$\overline{s}=\top \quad\land\quad s\mathrm{.EqOn}(f,g) \Rightarrow f=g$$$

Lean4

theorem eq_of_eqOn_set_dense {s : Set R} (hs : closure s = ⊤) {f g : R →ₙ+* S} (h : s.EqOn f g) : f = g :=
  eq_of_eqOn_set_top <| hs ▸ eqOn_set_closure h

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