spanningSetsIndex_eq_iff — Mathlib

English

The same relation as above: spanningSetsIndex(μ, x) = n holds exactly when x lies in the n-th disjointed piece.

Русский

Аналогично выше: равенство spanningSetsIndex(μ, x) = n точно означает, что x лежит в n-ой части disjointed.

LaTeX

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

Lean4

theorem spanningSetsIndex_eq_iff (μ : Measure α) [SigmaFinite μ] {x : α} {n : ℕ} :
    spanningSetsIndex μ x = n ↔ x ∈ disjointed (spanningSets μ) n := by
  convert Set.ext_iff.1 (preimage_spanningSetsIndex_singleton μ n) x

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