range_toSpanSingleton — Mathlib

English

Two semilinear maps f,g are equal on span s iff they are equal on s.

Русский

Два полилинейных отображения f,g равны на span s тогда и только тогда, когда они равны на s.

LaTeX

$$$Set.EqOn f g (span\ R\ s) \iff Set.EqOn f g s$$$

Lean4

/-- The range of `toSpanSingleton x` is the span of `x`. -/
theorem range_toSpanSingleton (x : M) : range (toSpanSingleton R M x) = .span R { x } :=
  SetLike.coe_injective (Submodule.span_singleton_eq_range R x).symm

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