instInnerRegularOfSigmaFinite — Mathlib

English

If μ is inner regular for compact LTTop and μ is sigma-finite, then μ is inner regular.

Русский

Если μ является внутренне регулярной по компактным множествам с LTTop и μ сигма-скалируема, то μ является внутренне регулярной.

LaTeX

$$$[InnerRegularCompactLTTop μ] \land [SigmaFinite μ] \Rightarrow μ \text{ is InnerRegular}$$$

Lean4

instance (priority := 80) [InnerRegularCompactLTTop μ] [SigmaFinite μ] : InnerRegular μ :=
  ⟨InnerRegularCompactLTTop.innerRegular.trans InnerRegularWRT.of_sigmaFinite⟩

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