average_zero_measure

Mathlib.MeasureTheory.Integral.Average

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

English

Reiteration: laverage of constant 1 on a nontrivial set equals 1.

Русский

Повтор: laverage от единицы по ненулевому множеству равна единице.

LaTeX

$$$\\laverage_{μ|s}(1)=1$$$

Lean4

@[simp]
theorem average_zero_measure (f : α → E) : ⨍ x, f x ∂(0 : Measure α) = 0 := by
  rw [average, smul_zero, integral_zero_measure]

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

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

Разделы

Аффилиация

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