finiteAt_nhds — Mathlib

English

If μ is a finite measure and c ≠ ∞ in ℝ≥0∞, then c • μ is finite.

Русский

Если μ — конечная мера и c ≠ ∞, то c • μ — конечная мера.

LaTeX

$$(μ : Measure α) [IsFiniteMeasure μ] \Rightarrow (c ≠ ∞) \Rightarrow IsFiniteMeasure (c • μ)$$

Lean4

theorem finiteAt_nhds [TopologicalSpace α] (μ : Measure α) [IsLocallyFiniteMeasure μ] (x : α) :
    μ.FiniteAtFilter (𝓝 x) :=
  IsLocallyFiniteMeasure.finiteAtNhds x

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