mem_ae_iff_prob_eq_one

Mathlib.MeasureTheory.Measure.Typeclasses.Probability

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

English

For MeasurableSet s, s ∈ ae μ iff μ s = 1.

Русский

Для измеримого множества s: s ∈ ae μ эквивалентно μ s = 1.

LaTeX

$$$\text{MeasurableSet}(s) \Rightarrow (s \in \mathrm{ae}(\mu) \iff \mu(s) = 1)$$$

Lean4

theorem mem_ae_iff_prob_eq_one (hs : MeasurableSet s) : s ∈ ae μ ↔ μ s = 1 :=
  mem_ae_iff.trans <| prob_compl_eq_zero_iff hs

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

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

Разделы

Аффилиация

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