English
If μ is inner regular with respect to p and μ(A) is finite, then μ|A is inner regular with respect to p on measurable sets.
Русский
Если μ имеет внутреннюю регулярность по p и μ(A) < ∞, то μ|A имеет внутреннюю регулярность по p на измеримых множеств.
LaTeX
$$$InnerRegularWRT(μ; p; MeasurableSet) \Rightarrow (μ|A) InnerRegularWRT p MeasurableSet \text{ при } μ(A) < ∞.$$$
Lean4
/-- If `μ` is inner regular for measurable finite measure sets with respect to some class of sets,
then its restriction to any finite measure set is also inner regular for measurable sets with
respect to the same class of sets. -/
theorem restrict_of_measure_ne_top (h : InnerRegularWRT μ p (fun s ↦ MeasurableSet s ∧ μ s ≠ ∞)) {A : Set α}
(hA : μ A ≠ ∞) : InnerRegularWRT (μ.restrict A) p (fun s ↦ MeasurableSet s) :=
by
have : Fact (μ A < ∞) := ⟨hA.lt_top⟩
exact (restrict h A).trans (of_imp (fun s hs ↦ ⟨hs, measure_ne_top _ _⟩))
