ae_cond_mem₀

Mathlib.Probability.ConditionalProbability

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.ae_cond_mem₀

English

For a NullMeasurableSet s with μ, almost every x in s belongs to s under μ|s.

Русский

Для нулево-меряемого множества s относительно μ почти все x в s принадлежат s под μ|s.

LaTeX

$$$(hs : NullMeasurableSet s μ) \\Rightarrow ∀ᵐ x ∂μ|s, x ∈ s$$$

Lean4

theorem ae_cond_mem₀ (hs : NullMeasurableSet s μ) : ∀ᵐ x ∂μ[|s], x ∈ s :=
  ae_smul_measure (ae_restrict_mem₀ hs) _

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

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

Разделы

Аффилиация

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