nonempty_inter_support_of_pos

Mathlib.MeasureTheory.Measure.Support

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

← MathLib Explorer

English

If μ(s) > 0, then s ∩ supp(μ) is nonempty.

Русский

Если μ(s) > 0, то s ∩ supp(μ) непусто.

LaTeX

$$0 < μ(s) \\Rightarrow (s \\cap \\mathrm{supp}(\\mu)).Nonempty$$

Lean4

theorem nonempty_inter_support_of_pos {s : Set X} (hμ : 0 < μ s) : (s ∩ μ.support).Nonempty :=
  by
  rw [← Set.not_disjoint_iff_nonempty_inter]
  contrapose! hμ
  exact μ.mono hμ.subset_compl_right |>.trans <| by simp

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

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

Разделы

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

Аффилиация

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