everywherePosSubset — Mathlib

English

The everywhere-positivity subset of a measurable set coincides with the set itself almost everywhere (under appropriate regularity assumptions).

Русский

Подмножество everywherePosSubset измеримо и совпадает с множеством почти всюду (при соответствующих предположениях регулярности).

LaTeX

$$$$ \\mu\\text{-a.e. }(\\mu.everywherePosSubset s) = s. $$$$

Lean4

/-- The everywhere positive subset of a set is the subset made of those points all of whose
neighborhoods have positive measure inside the set. -/
def everywherePosSubset (μ : Measure α) (s : Set α) : Set α :=
  {x | x ∈ s ∧ ∀ n ∈ 𝓝[s] x, 0 < μ n}

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