ext_on — Mathlib

English

If the subalgebra generated by s is dense in A and f,g agree on s, then f = g.

Русский

Если порождающая подалгебра s плотно заполнена в A и f, g совпадают на s, то f = g.

LaTeX

$$Dense(Algebra.adjoin_R(s)) ⇒ (EqOn f g s) ⇒ f = g$$

Lean4

/-- If the subalgebra generated by a set `s` is dense in the ambient module, then two continuous
algebra maps equal on `s` are equal. -/
theorem ext_on [T2Space B] {s : Set A} (hs : Dense (Algebra.adjoin R s : Set A)) {f g : A →A[R] B}
    (h : Set.EqOn f g s) : f = g :=
  ext fun x => eqOn_closure_adjoin h (hs x)

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