support_mem_ae — Mathlib

English

In a hereditarily Lindelöf space, the support of a measure μ is almost everywhere equal to the whole space in the sense of μ.

Русский

В пространства с наследуемым свойством Линдельёфа опора меры μ совпадает с пространством почти повсюду.

LaTeX

$$Support(μ) ∈ ae(μ)$$

Lean4

/-- In a hereditarily Lindelöf space, the support of a measure is conull. -/
theorem support_mem_ae : μ.support ∈ ae μ :=
  support_mem_ae_of_isLindelof <| HereditarilyLindelof_LindelofSets μ.supportᶜ

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