English
If μ is InnerRegularCompactLTTop, then its restriction to any set A is again InnerRegularCompactLTTop.
Русский
Если μ имеет InnerRegularCompactLTTop, то ограничение μ на любое множество A снова имеет InnerRegularCompactLTTop.
LaTeX
$$$[InnerRegularCompactLTTop μ]\\; A: Set α\\; \\Rightarrow InnerRegularCompactLTTop (μ.restrict A)$$$
Lean4
/-- If `μ` is inner regular for finite measure sets with respect to compact sets, then its
restriction to any set also is. -/
instance restrict [h : InnerRegularCompactLTTop μ] (A : Set α) : InnerRegularCompactLTTop (μ.restrict A) :=
⟨InnerRegularWRT.restrict h.innerRegular A⟩