exists_measurable_superset_ae_eq — Mathlib

English

Every null measurable set has a measurable superset that is equal to it almost everywhere.

Русский

Каждое нулево измеримое множество имеет измеримое надмножество, равное ему почти наверное.

LaTeX

$$$\\exists t \\supseteq s,\\ MeasurableSet t \\wedge t =^\\mu s$$$

Lean4

theorem exists_measurable_superset_ae_eq (h : NullMeasurableSet s μ) : ∃ t ⊇ s, MeasurableSet t ∧ t =ᵐ[μ] s :=
  by
  rcases h with ⟨t, htm, hst⟩
  refine ⟨t ∪ toMeasurable μ (s \ t), ?_, htm.union (measurableSet_toMeasurable _ _), ?_⟩
  · exact diff_subset_iff.1 (subset_toMeasurable _ _)
  · have : toMeasurable μ (s \ t) =ᵐ[μ] (∅ : Set α) := by simp [ae_le_set.1 hst.le]
    simpa only [union_empty] using hst.symm.union this

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