ae_neBot

Mathlib.MeasureTheory.Measure.Typeclasses.Probability

URI: https://scilib.ai/kg/mathlib#MeasureTheory.IsProbabilityMeasure.ae_neBot

English

For a probability measure μ, the a.e. filter ae μ is nontrivial (NeBot).

Русский

Для вероятностной меры μ фильтр почти всюду ae μ не тривиален (NeBot).

LaTeX

$$$\mathrm{NeBot}(\mathrm{ae}(\mu))$$$

Lean4

theorem ae_neBot [IsProbabilityMeasure μ] : NeBot (ae μ) :=
  inferInstance

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

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

Разделы

Аффилиация

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