ae_cond_mem

Mathlib.Probability.ConditionalProbability

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

English

For measurable s, almost everywhere with respect to cond μ s, x ∈ s.

Русский

Для измеримого s почти наверняка по μ|s верно x∈s.

LaTeX

$$$(hs : MeasurableSet s) \\Rightarrow ∀{p: Ω\\to Prop}, (∀ x, x∈s → p x) → (∀ᵐ x ∂μ|s, p x)$$$

Lean4

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

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

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

Разделы

Аффилиация

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