restrict_mass

Mathlib.MeasureTheory.Measure.FiniteMeasure

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

← MathLib Explorer

English

The total mass (or mass) of the restricted finite measure μ.restrict A equals μ(A).

Русский

Полная масса ограниченной меры μ.restrict A равна μ(A).

LaTeX

$$$ (\mu.restrict A).mass = \mu(A) $$$

Lean4

theorem restrict_mass (μ : FiniteMeasure Ω) (A : Set Ω) : (μ.restrict A).mass = μ A := by
  simp only [mass, restrict_apply μ A MeasurableSet.univ, univ_inter]

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

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

Разделы

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

Аффилиация

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