measure_lt_top_of_nhdsWithin — Mathlib

English

If s is compact and μ is finite at nhdsWithin x s for all x ∈ s, then μ(s) < ∞.

Русский

Если s компактно и для каждого x ∈ s мера μ в окрестности nhdsWithin x s конечна, то μ(s) < ∞.

LaTeX

$$$$\text{If } s \text{ is compact and } \forall x \in s,\; \mu(\mathcal{N}_s(x)) < \infty, \text{ then } \mu(s) < \infty.$$$$

Lean4

theorem measure_lt_top_of_nhdsWithin (h : IsCompact s) (hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝[s] x)) : μ s < ∞ :=
  IsCompact.induction_on h (by simp) (fun _ _ hst ht => (measure_mono hst).trans_lt ht)
    (fun s t hs ht => (measure_union_le s t).trans_lt (ENNReal.add_lt_top.2 ⟨hs, ht⟩)) hμ

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