measureDense_measurableSet — Mathlib

English

The completion of μ preserves measure-density: μ.completion.MeasureDense 𝒜 when μ.MeasureDense 𝒜.

Русский

Дополнение μ сохраняет measure-density: μ.completion.MeasureDense 𝒜 при μ.MeasureDense 𝒜.

LaTeX

$$$ \\mu.completion.MeasureDense 𝒜 $$$

Lean4

/-- The set of measurable sets is measure-dense. -/
theorem measureDense_measurableSet : μ.MeasureDense {s | MeasurableSet s}
    where
  measurable _ h := h
  approx s hs _ ε ε_pos := ⟨s, hs, by simpa⟩

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