instSigmaFiniteRestrictSigmaFiniteSet

English

The restriction of an s-finite measure μ to μ.sigmaFiniteSet is sigma-finite.

Русский

Ограничение сигма-финитной меры μ до μ.sigmaFiniteSet сигма-финитно.

LaTeX

$$$$\SigmaFinite(\mu\restriction\mu.sigmaFiniteSet).$$$$

Lean4

/-- The restriction of an s-finite measure `μ` to `μ.sigmaFiniteSet` is sigma-finite. -/
instance : SigmaFinite (μ.restrict μ.sigmaFiniteSet) :=
  by
  rw [Measure.sigmaFiniteSet]
  infer_instance

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