English
If two continuous semilinear maps agree on a set s, they agree on the closure of the span of s.
Русский
Если два непрерывных σ12-семилинейных отображения совпадают на множестве s, они совпадают на замыкании линейного замыкания s.
LaTeX
$$eqOn_closure_span [T2Space M2] {s : Set M1} {f g : M1 →SL[σ12] M2} (h : Set.EqOn f g s) : Set.EqOn (ContinuousLinearMap.funLike.coe f) (ContinuousLinearMap.funLike.coe g) (closure (Submodule.setLike.coe (Submodule.span R1 s)))$$
Lean4
/-- If the submodule generated by a set `s` is dense in the ambient module, then two continuous
linear maps equal on `s` are equal. -/
theorem ext_on [T2Space M₂] {s : Set M₁} (hs : Dense (Submodule.span R₁ s : Set M₁)) {f g : M₁ →SL[σ₁₂] M₂}
(h : Set.EqOn f g s) : f = g :=
ext fun x => eqOn_closure_span h (hs x)
