exists_measurable_superset_of_trim_eq_zero

English

If m.trim s = 0, there exists a measurable superset t with m t = 0.

Русский

Если m.trim s = 0, существует измеримое надмножество t с m t = 0.

LaTeX

$$$$ m^{\mathrm{trim}}(s) = 0 \Rightarrow \exists t,\; s \subseteq t \;\land\; MeasurableSet(t) \;\land\; m(t) = 0. $$$$

Lean4

theorem exists_measurable_superset_of_trim_eq_zero {m : OuterMeasure α} {s : Set α} (h : m.trim s = 0) :
    ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = 0 :=
  by
  rcases exists_measurable_superset_eq_trim m s with ⟨t, hst, ht, hm⟩
  exact ⟨t, hst, ht, h ▸ hm⟩

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