spanningSetsIndex — Mathlib

English

For each x ∈ α, spanningSetsIndex(μ, x) is the least natural number n such that x ∈ spanningSets(μ, n).

Русский

Для каждого x ∈ α spanningSetsIndex(μ, x) есть наименьшее натуральное число n такое, что x ∈ spanningSets(μ, n).

LaTeX

$$$spanningSetsIndex(\mu, x) = \min\{n\in\mathbb{N} : x \in spanningSets(\mu,n)\}$$$

Lean4

/-- `spanningSetsIndex μ x` is the least `n : ℕ` such that `x ∈ spanningSets μ n`. -/
noncomputable def spanningSetsIndex (μ : Measure α) [SigmaFinite μ] (x : α) : ℕ :=
  Nat.find <| iUnion_eq_univ_iff.1 (iUnion_spanningSets μ) x

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