measure_zero_of_nhdsWithin — Mathlib

English

If s is compact and every point a ∈ s has a neighborhood t ⊆ nhdsWithin a s with μ(t) = 0, then μ(s) = 0.

Русский

Если s компактно и для каждого a ∈ s существует окрестность t ⊆ nhdsWithin a s с μ(t) = 0, то μ(s) = 0.

LaTeX

$$$$\text{If } s \text{ is compact and } \forall a \in s,\; ∃ t ∈ \mathcal{N}_s(a),\; μ(t) = 0 \Rightarrow μ(s) = 0.$$$$

Lean4

theorem measure_zero_of_nhdsWithin (hs : IsCompact s) : (∀ a ∈ s, ∃ t ∈ 𝓝[s] a, μ t = 0) → μ s = 0 := by
  simpa only [← compl_mem_ae_iff] using hs.compl_mem_sets_of_nhdsWithin

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