mem_spanningSetsIndex — Mathlib

English

Every x lies in the spanning set corresponding to its index: x ∈ spanningSets(μ, spanningSetsIndex(μ, x)).

Русский

Каждый элемент x принадлежит соответствующему охватывающему множеству: x ∈ spanningSets(μ, spanningSetsIndex(μ, x)).

LaTeX

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

Lean4

theorem mem_spanningSetsIndex (μ : Measure α) [SigmaFinite μ] (x : α) : x ∈ spanningSets μ (spanningSetsIndex μ x) :=
  disjointed_subset _ _ (mem_disjointed_spanningSetsIndex μ x)

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