English
For a countable family μ_i of outer measures and a set s, there exists a measurable superset t such that μ_i t = (μ_i).trim s for all i.
Русский
Для счётной семейства μ_i внешних мер и множества s существует измеримое надмножество t, для которого μ_i t = (μ_i).trim s для всех i.
LaTeX
$$$$ \exists t, s \subseteq t \land MeasurableSet(t) \land \forall i, \mu_i(t) = (\mu_i).\mathrm{trim}(s). $$$$
Lean4
/-- If `μ i` is a countable family of outer measures, then for every set `s` there exists
a measurable set `t ⊇ s` such that `μ i t = (μ i).trim s` for all `i`. -/
theorem exists_measurable_superset_forall_eq_trim {ι} [Countable ι] (μ : ι → OuterMeasure α) (s : Set α) :
∃ t, s ⊆ t ∧ MeasurableSet t ∧ ∀ i, μ i t = (μ i).trim s :=
by
choose t hst ht hμt using fun i => (μ i).exists_measurable_superset_eq_trim s
replace hst := subset_iInter hst
replace ht := MeasurableSet.iInter ht
refine ⟨⋂ i, t i, hst, ht, fun i => le_antisymm ?_ ?_⟩
exacts [hμt i ▸ (μ i).mono (iInter_subset _ _), (measure_mono hst).trans_eq ((μ i).trim_eq ht)]
