isProbabilityMeasure_map_up

Mathlib.MeasureTheory.Measure.Typeclasses.Probability

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

English

The map under ULift.up of a probability measure is a probability measure.

Русский

Образ под ULift.up вероятностной меры — вероятностная мера.

LaTeX

$$$\mathrm{IsProbabilityMeasure}(\mathrm{map}\ {\mathrm{ULift}}\mathrm{up}\ mu)$$$

Lean4

instance isProbabilityMeasure_map_up : IsProbabilityMeasure (μ.map ULift.up) :=
  isProbabilityMeasure_map measurable_up.aemeasurable

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

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

Разделы

Аффилиация

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