dense_of_ae — Mathlib

English

If a property p holds μ-almost everywhere, then the set {x ∈ X | p(x)} is dense in X.

Русский

Если свойство p выполняется μ-почти повсюду, то множество {x ∈ X | p(x)} плотно в X.

LaTeX

$$$(\\forall x,\\ p(x))\\text{ holds a.e. w.r.t. } μ \\Rightarrow \\overline{\\{x\\in X : p(x)\\}} = X.$$$

Lean4

/-- A property satisfied almost everywhere is satisfied on a dense subset. -/
theorem dense_of_ae {p : X → Prop} (hp : ∀ᵐ x ∂μ, p x) : Dense {x | p x} :=
  by
  rw [dense_iff_closure_eq, closure_eq_compl_interior_compl, compl_univ_iff]
  exact μ.interior_eq_empty_of_null hp

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