add_sub_cancel

Mathlib.MeasureTheory.Measure.Sub

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.add_sub_cancel

← MathLib Explorer

English

If IsFinite ν and ν ≤ μ, then (μ + ν) − ν = μ.

Русский

Если IsFinite ν и ν ≤ μ, то (μ + ν) − ν = μ.

LaTeX

$$$[IsFiniteMeasure \\\\nu] \\\\Rightarrow (\\\\mu + \\\\nu) - \\\\nu = \\\\mu$$$

Lean4

@[simp]
protected theorem add_sub_cancel [IsFiniteMeasure ν] : μ + ν - ν = μ :=
  by
  ext1 s hs
  rw [sub_apply hs (Measure.le_add_left (le_refl _)), add_apply, ENNReal.add_sub_cancel_right (measure_ne_top ν s)]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru