measureReal_def

Mathlib.MeasureTheory.Measure.MeasureSpaceDef

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

English

For any measure μ and any set s, the real-valued part of μ on s equals the real value of μ on s.

Русский

Для любой меры μ и любого множества s действительная часть μ на s равна числу (μ(s)).toReal.

LaTeX

$$$\operatorname{toReal}(\mu(s)) = \mu^{\text{real}}(s)$$$

Lean4

theorem measureReal_def {α : Type*} {m : MeasurableSpace α} (μ : Measure α) (s : Set α) : μ.real s = (μ s).toReal :=
  rfl

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

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

Разделы

Аффилиация

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