add_right — Mathlib

English

Let μ, ν, ν' be measures on α. If μ is absolutely continuous with respect to ν, then μ is absolutely continuous with respect to ν + ν'.

Русский

Пусть μ, ν, ν' — меры на α. Если μ абсолютно непрерывна относительно ν, то μ абсолютно непрерывна относительно ν + ν'.

LaTeX

$$$\mu \ll \nu \Rightarrow \mu \ll \nu + \nu'$$$

Lean4

theorem add_right (h1 : μ ≪ ν) (ν' : Measure α) : μ ≪ ν + ν' :=
  by
  intro s hs
  simp only [coe_add, Pi.add_apply, add_eq_zero] at hs ⊢
  exact h1 hs.1

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