sub — Mathlib

English

If v₁ ≪ᵥ w and v₂ ≪ᵥ w, then v₁ − v₂ ≪ᵥ w.

Русский

Если v₁ ≪ᵥ w и v₂ ≪ᵥ w, тогда v₁ − v₂ ≪ᵥ w.

LaTeX

$$hv₁ : v₁ ≪ᵥ w → hv₂ : v₂ ≪ᵥ w → (v₁ - v₂) ≪ᵥ w$$

Lean4

theorem sub {M : Type*} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] {v₁ v₂ : VectorMeasure α M}
    {w : VectorMeasure α N} (hv₁ : v₁ ≪ᵥ w) (hv₂ : v₂ ≪ᵥ w) : v₁ - v₂ ≪ᵥ w :=
  by
  intro s hs
  rw [sub_apply, hv₁ hs, hv₂ hs, zero_sub, neg_zero]

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