eqOn_closure_span — Mathlib

English

If the submodule generated by a set s is dense, equality on s implies equality of maps on the whole M1.

Русский

Если подмодуль, порожденный s, плотный, равенство на s влечет равенство отображений на всём M1.

LaTeX

$$ext_on [T2Space M2] {s : Set M1} {f g : M1 →SL[σ12] M2} (hs: Dense (Submodule.span R1 s : Set M1)) (h: Set.EqOn f g s) : f = g$$

Lean4

/-- If two continuous linear maps are equal on a set `s`, then they are equal on the closure
of the `Submodule.span` of this set. -/
theorem eqOn_closure_span [T2Space M₂] {s : Set M₁} {f g : M₁ →SL[σ₁₂] M₂} (h : Set.EqOn f g s) :
    Set.EqOn f g (closure (Submodule.span R₁ s : Set M₁)) :=
  (LinearMap.eqOn_span' h).closure f.continuous g.continuous

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