support_mem_ae_of_isLindelof — Mathlib

English

If the complement of the support is Lindelöf, then the support is conull (i.e., its complement is negligible).

Русский

Если дополнение опоры Линдельофово, то опора конулева (соотношение к μ).

LaTeX

$$IsLindelof(\\mathrm{supp}(\\mu)^{c}) \\Rightarrow \\mathrm{supp}(\\mu) \\in \\mathrm{ae}(\\mu)$$

Lean4

/-- If the complement of the support is Lindelöf, then the support of a measure is conull. -/
theorem support_mem_ae_of_isLindelof (h : IsLindelof μ.supportᶜ) : μ.support ∈ ae μ :=
  by
  refine compl_compl μ.support ▸ h.compl_mem_sets_of_nhdsWithin fun s hs ↦ ?_
  simpa [compl_mem_ae_iff, isOpen_compl_support.nhdsWithin_eq hs] using notMem_support_iff_exists.mp hs

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