withDensity_one

Mathlib.MeasureTheory.Measure.WithDensity

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

English

If the density is identically one, μ with density one equals μ.

Русский

Если плотность равна единице на всей области, то μ с плотностью единицы равна μ.

LaTeX

$$$\\mu\\_f = \\mu$ при $f \\equiv 1$$$

Lean4

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

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

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

Разделы

Аффилиация

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