withDensity_zero_left

Mathlib.MeasureTheory.Measure.WithDensity

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

English

The density of the zero measure with any density f is the zero measure.

Русский

Плотность нулевой меры при любой плотности f равна нулевой мере.

LaTeX

$$$0\text{: Measure } \Rightarrow (0:\text{ Measure } \alpha).withDensity f = 0$$$

Lean4

@[simp]
theorem withDensity_zero_left (f : α → ℝ≥0∞) : (0 : Measure α).withDensity f = 0 :=
  by
  ext s hs
  rw [withDensity_apply _ hs]
  simp

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

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

Разделы

Аффилиация

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