withDensity_zero

Mathlib.MeasureTheory.Measure.WithDensity

URI: https://scilib.ai/kg/mathlib#MeasureTheory.withDensity_zero

English

If the density is identically zero, the resulting measure is the zero measure.

Русский

Если плотность нулевая на всей области, полученная мера равна нулевой мере.

LaTeX

$$$\\mu\\_f = 0$$$

Lean4

@[simp]
theorem withDensity_zero : μ.withDensity 0 = 0 := by
  ext1 s hs
  simp [withDensity_apply _ hs]

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

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

Разделы

Аффилиация

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