setLAverage_one

Mathlib.MeasureTheory.Integral.Average

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

English

As a corollary of setLAverage_const, if μ(s) ≠ 0 and μ(s) ≠ ∞, then laverage of 1 equals 1.

Русский

Следствие: если μ(s) ≠ 0 и μ(s) ≠ ∞, то лаverage единицы равна единице.

LaTeX

$$$\\laverage_{μ|s}(1) = 1$ при $μ(s) ≠ 0$ и $μ(s) ≠ ∞$$$

Lean4

theorem setLAverage_one (hs₀ : μ s ≠ 0) (hs : μ s ≠ ∞) : ⨍⁻ _x in s, (1 : ℝ≥0∞) ∂μ = 1 :=
  setLAverage_const hs₀ hs _

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

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

Разделы

Аффилиация

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