instIsFiniteMeasureOnCompactsRestrict

English

Restriction of μ to any set s preserves the finiteness-on-compacts property.

Русский

Ограничение меры μ на множество s сохраняет свойство конечности на компактных подмножествах.

LaTeX

$$$IsFiniteMeasureOnCompacts (\mu\restrict s)$$$

Lean4

instance instIsFiniteMeasureOnCompactsRestrict [TopologicalSpace α] {μ : Measure α} [IsFiniteMeasureOnCompacts μ]
    {s : Set α} : IsFiniteMeasureOnCompacts (μ.restrict s) :=
  ⟨fun _k hk ↦ (restrict_apply_le _ _).trans_lt hk.measure_lt_top⟩

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