English
The Borel sigma-algebra on G is contained in the Carathéodory-measurable sets with respect to μ.outerMeasure.
Русский
Борелевская сигма-алгебра на G содержится в множествах, измеримых по карاثеодори μ.outerMeasure.
LaTeX
$$$$\\mathcal{B}(G) \\subseteq \\mathcal{M}_{μ.outerMeasure.caratheodory}.$$$$
Lean4
/-- For the outer measure coming from a content, all Borel sets are measurable. -/
theorem borel_le_caratheodory : S ≤ μ.outerMeasure.caratheodory :=
by
rw [BorelSpace.measurable_eq (α := G)]
refine MeasurableSpace.generateFrom_le ?_
intro U hU
rw [μ.outerMeasure_caratheodory]
intro U'
rw [μ.outerMeasure_of_isOpen ((U' : Set G) ∩ U) (U'.isOpen.inter hU)]
simp only [innerContent, iSup_subtype']
rw [Opens.coe_mk]
haveI : Nonempty { L : Compacts G // (L : Set G) ⊆ U' ∩ U } := ⟨⟨⊥, empty_subset _⟩⟩
rw [ENNReal.iSup_add]
refine iSup_le ?_
rintro ⟨L, hL⟩
let L' : Compacts G := ⟨closure L, L.isCompact.closure⟩
suffices μ L' + μ.outerMeasure (↑U' \ U) ≤ μ.outerMeasure U'
by
have A : μ L ≤ μ L' := μ.mono _ _ subset_closure
exact (add_le_add_right A _).trans this
simp only [subset_inter_iff] at hL
have hL'U : (L' : Set G) ⊆ U := IsCompact.closure_subset_of_isOpen L.2 hU hL.2
have hL'U' : (L' : Set G) ⊆ (U' : Set G) := IsCompact.closure_subset_of_isOpen L.2 U'.2 hL.1
have : ↑U' \ U ⊆ U' \ L' := diff_subset_diff_right hL'U
grw [this]
rw [μ.outerMeasure_of_isOpen (↑U' \ L') (IsOpen.sdiff U'.2 isClosed_closure)]
simp only [innerContent, iSup_subtype']
rw [Opens.coe_mk]
haveI : Nonempty { M : Compacts G // (M : Set G) ⊆ ↑U' \ closure L } := ⟨⟨⊥, empty_subset _⟩⟩
rw [ENNReal.add_iSup]
refine iSup_le ?_
rintro ⟨M, hM⟩
let M' : Compacts G := ⟨closure M, M.isCompact.closure⟩
suffices μ L' + μ M' ≤ μ.outerMeasure U'
by
have A : μ M ≤ μ M' := μ.mono _ _ subset_closure
exact (add_le_add_left A _).trans this
have hM' : (M' : Set G) ⊆ U' \ L' := IsCompact.closure_subset_of_isOpen M.2 (IsOpen.sdiff U'.2 isClosed_closure) hM
have : (↑(L' ⊔ M') : Set G) ⊆ U' :=
by
simp only [Compacts.coe_sup, union_subset_iff, hL'U', true_and]
exact hM'.trans diff_subset
rw [μ.outerMeasure_of_isOpen (↑U') U'.2]
refine le_trans (ge_of_eq ?_) (μ.le_innerContent _ _ this)
exact μ.sup_disjoint L' M' (subset_diff.1 hM').2.symm isClosed_closure isClosed_closure
