eqOn_closure_adjoin — Mathlib

English

If two continuous A-homomorphisms f and g agree on a set s, they agree on the closure of the subalgebra generated by s.

Русский

Если два непрерывных гомоморфизма A-гомоморфизмов f и g совпадают на множестве s, то они совпадают на замыкании подалгебры, порождаемой s.

LaTeX

$$$\\text{EqOn}(f,g,s) \\Rightarrow \\text{EqOn}(f,g,\\overline{\\text{Algebra.adjoin}_R(s)}).$$$

Lean4

/-- If two continuous algebra maps are equal on a set `s`, then they are equal on the closure
of the `Algebra.adjoin` of this set. -/
theorem eqOn_closure_adjoin [T2Space B] {s : Set A} {f g : A →A[R] B} (h : Set.EqOn f g s) :
    Set.EqOn f g (closure (Algebra.adjoin R s : Set A)) :=
  Set.EqOn.closure (AlgHom.eqOn_adjoin_iff.mpr h) f.continuous g.continuous

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