eqOn_span — Mathlib

English

If s generates the whole module and two linear maps agree on s, then they agree on all of the module.

Русский

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

LaTeX

$$Extensibility_on_span_condition$$

Lean4

/-- If two linear maps are equal on a set `s`, then they are equal on `Submodule.span s`.

See also `LinearMap.eqOn_span'` for a version using `Set.EqOn`. -/
theorem eqOn_span {s : Set M} {f g : F} (H : Set.EqOn f g s) ⦃x⦄ (h : x ∈ span R s) : f x = g x :=
  eqOn_span' H h

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