English
For any set s, there exists a measurable superset t with s ⊆ t and m t = m.trim s.
Русский
Для любого множества s существует измеримое надмножество t с s ⊆ t и m t = m.trim s.
LaTeX
$$$$ \exists t,\; s \subseteq t \;\land\; MeasurableSet(t) \;\land\; m(t) = m^{\mathrm{trim}}(s). $$$$
Lean4
theorem exists_measurable_superset_eq_trim (m : OuterMeasure α) (s : Set α) :
∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = m.trim s :=
by
simp only [trim_eq_iInf]; set ms := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), m t
by_cases hs : ms = ∞
· simp only [hs]
simp only [iInf_eq_top, ms] at hs
exact ⟨univ, subset_univ s, MeasurableSet.univ, hs _ (subset_univ s) MeasurableSet.univ⟩
· have : ∀ r > ms, ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < r :=
by
intro r hs
have : ∃ t, MeasurableSet t ∧ s ⊆ t ∧ m t < r := by simpa [ms, iInf_lt_iff] using hs
rcases this with ⟨t, hmt, hin, hlt⟩
exists t
have : ∀ n : ℕ, ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < ms + (n : ℝ≥0∞)⁻¹ :=
by
intro n
refine this _ (ENNReal.lt_add_right hs ?_)
simp
choose t hsub hm hm' using this
refine ⟨⋂ n, t n, subset_iInter hsub, MeasurableSet.iInter hm, ?_⟩
have : Tendsto (fun n : ℕ => ms + (n : ℝ≥0∞)⁻¹) atTop (𝓝 (ms + 0)) :=
tendsto_const_nhds.add ENNReal.tendsto_inv_nat_nhds_zero
rw [add_zero] at this
refine le_antisymm (ge_of_tendsto' this fun n => ?_) ?_
· exact le_trans (measure_mono <| iInter_subset t n) (hm' n).le
· refine iInf_le_of_le (⋂ n, t n) ?_
refine iInf_le_of_le (subset_iInter hsub) ?_
exact iInf_le _ (MeasurableSet.iInter hm)
