support_eq_univ — Mathlib

English

If every nonempty open set has positive measure, then the support of μ is the whole space X.

Русский

Если каждое непустое открытое множество имеет положительную меру, то опора μ совпадает с всей пространством X.

LaTeX

$$\\text{If } \\forall U \\text{ open}, U \\neq \\emptyset \\Rightarrow \\mu(U) > 0, \\quad \\mathrm{supp}(\\mu) = X.$$

Lean4

theorem support_eq_univ [μ.IsOpenPosMeasure] : μ.support = Set.univ := by
  simpa [Set.eq_univ_iff_forall, mem_support_iff_forall] using fun _ _ ↦ μ.measure_pos_of_mem_nhds

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