isLocallyFiniteMeasure_of_le — Mathlib

English

If ν ≤ μ and μ is locally finite, then ν is locally finite.

Русский

Если ν ≤ μ и μ локально конечна, то ν также локально конечна.

LaTeX

$$$$\nu \le \mu \quad\text{and}\quad \text{IsLocallyFiniteMeasure}(\mu) \implies \text{IsLocallyFiniteMeasure}(\nu).$$$$

Lean4

theorem isLocallyFiniteMeasure_of_le [TopologicalSpace α] {_m : MeasurableSpace α} {μ ν : Measure α}
    [H : IsLocallyFiniteMeasure μ] (h : ν ≤ μ) : IsLocallyFiniteMeasure ν :=
  let F := H.finiteAtNhds
  ⟨fun x => (F x).measure_mono h⟩

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