exists_countable_measureDense — Mathlib

English

If a measure μ is separable, there exists a countable family 𝒜 of sets such that μ is measure-dense with respect to 𝒜.

Русский

Если мера μ является разделимой, существует счетная семейство множеств 𝒜, такое что μ плотна по 𝒜.

LaTeX

$$$$\\exists 𝒜\\; (𝒜\\text{ Countable}) \\wedge μ.\\text{MeasureDense } 𝒜.$$$$

Lean4

/-- By definition, a separable measure admits a countable and measure-dense family of sets. -/
theorem exists_countable_measureDense [IsSeparable μ] : ∃ 𝒜, 𝒜.Countable ∧ μ.MeasureDense 𝒜 :=
  IsSeparable.exists_countable_measureDense

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