ae_mem_iff_measure_eq — Mathlib

English

For finite μ and NullMeasurableSet s μ, the μ-ae membership in s is equivalent to μ(s) = μ(univ).

Русский

Для конечной μ и NullMeasurableSet s μ, membership a ∈ s μ-почти-верно тогда и только тогда, когда μ(s) = μ(univ).

LaTeX

$$$(\text{NullMeasurableSet}(s, \mu)) \Rightarrow (\forall a, a \in s) \text{ μ-ae} \iff \mu(s) = \mu(\mathrm{univ})$$

Lean4

theorem ae_mem_iff_measure_eq [IsFiniteMeasure μ] {s : Set α} (hs : NullMeasurableSet s μ) :
    (∀ᵐ a ∂μ, a ∈ s) ↔ μ s = μ univ :=
  ae_iff_measure_eq hs

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