nhds_isMeasurablyGenerated — Mathlib

English

If μ(frontier(s)) = 0, then μ(interior(s)) = μ(s).

Русский

Если μ( frontier(s) ) = 0, то μ( interior(s) ) = μ(s).

LaTeX

$$$\\mu(\\operatorname{frontier}(s)) = 0 \\Rightarrow \\mu(\\operatorname{interior}(s)) = \\mu(s).$$$

Lean4

instance nhds_isMeasurablyGenerated (a : α) : (𝓝 a).IsMeasurablyGenerated :=
  by
  rw [nhds, iInf_subtype']
  refine @Filter.iInf_isMeasurablyGenerated α _ _ _ fun i => ?_
  exact i.2.2.measurableSet.principal_isMeasurablyGenerated

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