exists_measurable_superset — Mathlib

English

For every μ and s there exists t ⊇ s with t measurable and μ t = μ s.

Русский

Для любого μ и s существует t ⊇ s, которое измеримо и μ t = μ s.

LaTeX

$$$\exists t, s \subseteq t \wedge MeasurableSet t \wedge μ t = μ s$$$

Lean4

/-- For every set there exists a measurable superset of the same measure. -/
theorem exists_measurable_superset (μ : Measure α) (s : Set α) : ∃ t, s ⊆ t ∧ MeasurableSet t ∧ μ t = μ s := by
  simpa only [← measure_eq_trim] using μ.toOuterMeasure.exists_measurable_superset_eq_trim s

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