measure_eq_one_iff_eq_univ — Mathlib

English

If F is closed and μ is a probability measure, then μ(F) = 1 if and only if F = univ.

Русский

Если F замкнуто и μ — вероятностьная мера, то μ(F) = 1 тогда и только тогда, когда F = univ.

LaTeX

$$$\\forall F,\\ [\\text{OpensMeasurableSpace }X] [\\text{Measure } μ] [\\text{IsProbabilityMeasure } μ],\\; IsClosed F \\rightarrow (μ(F) = 1 \\iff F = \\mathrm{univ}).$$$

Lean4

theorem _root_.IsClosed.measure_eq_one_iff_eq_univ [OpensMeasurableSpace X] [IsProbabilityMeasure μ] (hF : IsClosed F) :
    μ F = 1 ↔ F = univ := by rw [← measure_univ (μ := μ), hF.measure_eq_univ_iff_eq]

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