preimage_spanningSetsIndex_singleton

English

For each x ∈ α and n ∈ ℕ, spanningSetsIndex(μ, x) = n if and only if x belongs to the n-th disjointed piece of the spanning family.

Русский

Для каждого x и n ∈ ℕ равенство spanningSetsIndex(μ, x) = n эквивалентно тому, что x принадлежит члену разбиения на основе n-го элемента семейства spanningSets μ.

LaTeX

$$$spanningSetsIndex(\mu, x) = n \iff x \in disjointed(\mathrm{spanningSets}(\mu), n)$$$

Lean4

theorem preimage_spanningSetsIndex_singleton (μ : Measure α) [SigmaFinite μ] (n : ℕ) :
    spanningSetsIndex μ ⁻¹' { n } = disjointed (spanningSets μ) n :=
  preimage_find_eq_disjointed _ _ _

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