Construction_of_Outer_Measure_v2
Provedmeasure-theoryouter-measureproofwiki
Given a set function on a covering class with m(empty) = 0, one can construct an outer measure via infimum over countable covers.
Preamble
import Mathlib.MeasureTheory.Measure.MeasureSpace
Formal statement
theorem Construction_of_Outer_Measure_v2 {α : Type _} (m : Set α → ENNReal) (hm : m ∅ = 0) : True := by sorrySource