span_neg — Mathlib

English

Span is invariant under negation: the span of -s equals the span of s.

Русский

Спан инвариант по отрицанию: span(-s) = span(s).

LaTeX

$$$\operatorname{span}_{R}(-s) = \operatorname{span}_{R}(s)$$$

Lean4

@[simp]
theorem span_neg (s : Set M) : span R (-s) = span R s :=
  calc
    span R (-s) = span R ((-LinearMap.id : M →ₗ[R] M) '' s) := by simp
    _ = map (-LinearMap.id) (span R s) := (map_span (-LinearMap.id) _).symm
    _ = span R s := by simp

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