coeFn_def

Mathlib.MeasureTheory.Measure.FiniteMeasure

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

English

The evaluation map of a FiniteMeasure μ is the NNReal-valued function s ↦ ((μ : Measure Ω) s).toNNReal.

Русский

Оценочная функция конечной меры μ равна s ↦ ((μ : Measure Ω) s).toNNReal.

LaTeX

$$μ = fun s ↦ ((μ : Measure Ω) s).toNNReal$$

Lean4

theorem coeFn_def (μ : FiniteMeasure Ω) : μ = fun s ↦ ((μ : Measure Ω) s).toNNReal :=
  rfl

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

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

Разделы

Аффилиация

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