measure_eq_zero_or_top_of_subset_compl_sigmaFiniteSet

English

If a subset t lies inside the complement of μ.sigmaFiniteSet, then μ t is either 0 or ∞.

Русский

Если t ⊆ (μ.sigmaFiniteSet)ᶜ, то μ t ∈ {0, ∞}.

LaTeX

$$$$\mu t = 0 \quad\text{or}\quad \mu t = \infty.$$$$

Lean4

theorem measure_eq_zero_or_top_of_subset_compl_sigmaFiniteSet [SFinite μ] (ht_subset : t ⊆ μ.sigmaFiniteSetᶜ) :
    μ t = 0 ∨ μ t = ∞ := by
  rw [or_iff_not_imp_left]
  exact measure_eq_top_of_subset_compl_sigmaFiniteSetWRT ht_subset

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