instIsLocallyFiniteMeasure — Mathlib

English

If α has a topological structure and μ is locally finite, then μ.singularPart ν is locally finite.

Русский

Если α имеет топологическое пространство и μ локально конечна, то μ.singularPart ν локально конечна.

LaTeX

$$$$ [TopologicalSpace α] \ [IsLocallyFiniteMeasure μ] \Rightarrow IsLocallyFiniteMeasure(μ.singularPart ν) $$$$

Lean4

instance instIsLocallyFiniteMeasure [TopologicalSpace α] [IsLocallyFiniteMeasure μ] :
    IsLocallyFiniteMeasure (μ.singularPart ν) :=
  isLocallyFiniteMeasure_of_le <| singularPart_le μ ν

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