neg_right — Mathlib

English

The zero vector measure is absolutely continuous with respect to any w.

Русский

Нулевая векторная мера абсолютно непривязана к любой w.

LaTeX

$$∀ w, (0 : VectorMeasure α M) ≪ᵥ w$$

Lean4

theorem neg_right {N : Type*} [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] {v : VectorMeasure α M}
    {w : VectorMeasure α N} (h : v ≪ᵥ w) : v ≪ᵥ -w := by
  intro s hs
  rw [neg_apply, neg_eq_zero] at hs
  exact h hs

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