isLocallyFiniteMeasureSMulNNReal — Mathlib

English

The family of sets {s | IsOpen s ∧ μ s < ∞} forms a topological basis when μ is locally finite.

Русский

Семейство множест {s | IsOpen s ∧ μ s < ∞} образует топологический базис, если μ локально конечна.

LaTeX

$$TopologicalSpace.IsTopologicalBasis {s | IsOpen s ∧ μ s < ∞}$$

Lean4

instance isLocallyFiniteMeasureSMulNNReal [TopologicalSpace α] (μ : Measure α) [IsLocallyFiniteMeasure μ] (c : ℝ≥0) :
    IsLocallyFiniteMeasure (c • μ) := by
  refine ⟨fun x => ?_⟩
  rcases μ.exists_isOpen_measure_lt_top x with ⟨o, xo, o_open, μo⟩
  refine ⟨o, o_open.mem_nhds xo, ?_⟩
  apply ENNReal.mul_lt_top _ μo
  simp

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