testAgainstNN_one

Mathlib.MeasureTheory.Measure.FiniteMeasure

URI: https://scilib.ai/kg/mathlib#MeasureTheory.FiniteMeasure.testAgainstNN_one

← MathLib Explorer

English

For any finite measure μ, μ.testAgainstNN 1 equals μ.mass.

Русский

Для любой конечной меры μ, μ.testAgainstNN 1 равно μ.mass.

LaTeX

$$$\mu.testAgainstNN 1 = \mu.mass$$$

Lean4

@[simp]
theorem testAgainstNN_one (μ : FiniteMeasure Ω) : μ.testAgainstNN 1 = μ.mass :=
  by
  simp only [testAgainstNN, coe_one, Pi.one_apply, ENNReal.coe_one, lintegral_one]
  rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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