restrict_of_measure_ne_top — Mathlib

English

If μ is regular and A has finite measure, then the restricted measure μ.restrict A is regular.

Русский

Если μ регулярна и A имеет конечную меру, то ограниченная мера μ.restrict A регулярна.

LaTeX

$$$\\mu|_{A} \\text{ regular if } \\mu(A) < \\infty.$$$

Lean4

/-- The restriction of a regular measure to a set of finite measure is regular. -/
theorem restrict_of_measure_ne_top [R1Space α] [BorelSpace α] [Regular μ] {A : Set α} (h'A : μ A ≠ ∞) :
    Regular (μ.restrict A) :=
  by
  have : WeaklyRegular (μ.restrict A) := WeaklyRegular.restrict_of_measure_ne_top h'A
  constructor
  intro V hV r hr
  have R : restrict μ A V ≠ ∞ := by
    rw [restrict_apply hV.measurableSet]
    exact ((measure_mono inter_subset_right).trans_lt h'A.lt_top).ne
  exact MeasurableSet.exists_lt_isCompact_of_ne_top hV.measurableSet R hr

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