span_neg_eq_neg — Mathlib

English

Taking the span commutes with negation: span_R(-s) = - span_R(s) for any set s.

Русский

Операция замыкания линейной оболочки над множеством и отрицание коммутируют: span_R(-s) = - span_R(s).

LaTeX

$$$\operatorname{span}_R(-s) = -\operatorname{span}_R(s)$$$

Lean4

theorem span_neg_eq_neg (s : Set M) : span R (-s) = -span R s :=
  by
  apply le_antisymm
  · rw [span_le, coe_set_neg, ← Set.neg_subset, neg_neg]
    exact subset_span
  · rw [neg_le, span_le, coe_set_neg, ← Set.neg_subset]
    exact subset_span

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