subset_compl_support_of_isOpen

Mathlib.MeasureTheory.Measure.Support

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

← MathLib Explorer

English

If t is open and μ(t) = 0, then t is contained in the complement of the support.

Русский

Если t открыто и μ(t) = 0, то t ⊆ supp(μ)^c.

LaTeX

$$IsOpen(t) \\wedge \\mu(t) = 0 \\Rightarrow t \\subseteq \\mathrm{supp}(\\mu)^{c}$$

Lean4

theorem subset_compl_support_of_isOpen {t : Set X} (ht : IsOpen t) (h : μ t = 0) : t ⊆ μ.supportᶜ := fun _ hx ↦
  notMem_support_iff_exists.mpr ⟨t, ht.mem_nhds hx, h⟩

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

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

Разделы

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

Аффилиация

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