support_subset_of_isClosed

Mathlib.MeasureTheory.Measure.Support

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.support_subset_of_isClosed

← MathLib Explorer

English

If t is closed and t ∈ ae μ, then the support of μ is contained in t.

Русский

Если t замкнуто и t ∈ ae μ, то опора μ ⊆ t.

LaTeX

$$IsClosed(t) \\wedge t \\in \\mathrm{ae}(\\mu) \\Rightarrow \\mathrm{supp}(\\mu) \\subseteq t$$

Lean4

theorem support_subset_of_isClosed {t : Set X} (ht : IsClosed t) (h : t ∈ ae μ) : μ.support ⊆ t :=
  Set.compl_subset_compl.mp <| subset_compl_support_of_isOpen ht.isOpen_compl h

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru