restrict_compl_sigmaFiniteSet_eq_zero_or_top

English

For any μ and ν with ν finite, the restriction of μ to the complement of σFiniteSetWRT(ν) takes only two values: 0 or ∞.

Русский

Для любых μ и ν с ν конечной ограничение μ к дополнению σFiniteSetWRT(ν) принимает только 0 или ∞.

LaTeX

$$$$\mu\restriction\left(\mu.sigmaFiniteSetWRT(\nu)\right)^{c} (s) = 0 \quad\text{or}\quad = \infty.$$$$

Lean4

/-- The measure `μ.restrict μ.sigmaFiniteSetᶜ` takes only two values: 0 and ∞ . -/
theorem restrict_compl_sigmaFiniteSet_eq_zero_or_top (μ : Measure α) [SFinite μ] (s : Set α) :
    μ.restrict μ.sigmaFiniteSetᶜ s = 0 ∨ μ.restrict μ.sigmaFiniteSetᶜ s = ∞ :=
  by
  rw [Measure.restrict_apply' measurableSet_sigmaFiniteSet.compl]
  exact measure_eq_zero_or_top_of_subset_compl_sigmaFiniteSet Set.inter_subset_right

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