restrict — Mathlib

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⟩

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