mem_disjointed_spanningSetsIndex — Mathlib

English

For any x ∈ α, x lies in the disjointed piece at the index given by spanningSetsIndex(μ, x).

Русский

Для любого x ∈ α x принадлежит соответствующей disjointed-части с индексом spanningSetsIndex(μ, x).

LaTeX

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

Lean4

theorem mem_disjointed_spanningSetsIndex (μ : Measure α) [SigmaFinite μ] (x : α) :
    x ∈ disjointed (spanningSets μ) (spanningSetsIndex μ x) :=
  (spanningSetsIndex_eq_iff μ).1 rfl

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