restrict_of_measure_ne_top — Mathlib

English

Restricting a weakly regular measure to a measurable finite-set yields a weakly regular measure again.

Русский

Ограничение слабой регулярной меры до измеримого множества с конечной мерой снова дает слабую регулярность.

LaTeX

$$$\forall A:\ Measurable A, μ(A) < ∞ \Rightarrow (μ\restriction A) \text{ is WeaklyRegular}$$$

Lean4

/-- The restriction of a weakly regular measure to a measurable set of finite measure is
weakly regular. -/
theorem restrict_of_measure_ne_top [BorelSpace α] [WeaklyRegular μ] {A : Set α} (h'A : μ A ≠ ∞) :
    WeaklyRegular (μ.restrict A) := by
  haveI : Fact (μ A < ∞) := ⟨h'A.lt_top⟩
  refine InnerRegularWRT.weaklyRegular_of_finite (μ.restrict A) (fun V V_open r hr ↦ ?_)
  have : InnerRegularWRT (μ.restrict A) IsClosed (fun s ↦ MeasurableSet s) :=
    InnerRegularWRT.restrict_of_measure_ne_top innerRegular_measurable h'A
  exact this V_open.measurableSet r hr

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