ofMeasurable_apply — Mathlib

English

For every set s there exists a measurable superset t ⊇ s with the same outer-measure; μ t = μ s.

Русский

Для любого множества s существует измеримое надмножество t ⊇ s такое, что μ t = μ s.

LaTeX

$$$\exists t, s \subseteq t \wedge MeasurableSet t \wedge μ t = μ s$$$

Lean4

theorem ofMeasurable_apply {m : ∀ s : Set α, MeasurableSet s → ℝ≥0∞} {m0 : m ∅ MeasurableSet.empty = 0}
    {mU :
      ∀ ⦃f : ℕ → Set α⦄ (h : ∀ i, MeasurableSet (f i)),
        Pairwise (Disjoint on f) → m (⋃ i, f i) (MeasurableSet.iUnion h) = ∑' i, m (f i) (h i)}
    (s : Set α) (hs : MeasurableSet s) : ofMeasurable m m0 mU s = m s hs :=
  inducedOuterMeasure_eq m0 mU hs

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