neg_left — Mathlib

English

If v ⟂ᵥ w then -v ⟂ᵥ w.

Русский

Если v ⟂ᵥ w, то -v ⟂ᵥ w.

LaTeX

$$$ v \\perp_{\\mathcal{V}} w \\Rightarrow (-v) \\perp_{\\mathcal{V}} w $$$

Lean4

theorem neg_left {M : Type*} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] {v : VectorMeasure α M}
    {w : VectorMeasure α N} (h : v ⟂ᵥ w) : -v ⟂ᵥ w :=
  by
  obtain ⟨u, hmu, hu₁, hu₂⟩ := h
  refine ⟨u, hmu, fun s hs => ?_, hu₂⟩
  rw [neg_apply v s, neg_eq_zero]
  exact hu₁ s hs

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