neg_left_iff — Mathlib

English

The negation correlates: -v ⟂ᵥ w iff v ⟂ᵥ w.

Русский

Отрицание имеет эквивалентность: -v ⟂ᵥ w эквивалентно v ⟂ᵥ w.

LaTeX

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

Lean4

@[simp]
theorem neg_left_iff {M : Type*} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] {v : VectorMeasure α M}
    {w : VectorMeasure α N} : -v ⟂ᵥ w ↔ v ⟂ᵥ w :=
  ⟨fun h => neg_neg v ▸ h.neg_left, neg_left⟩

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