eventually_mem_spanningSets — Mathlib

English

For every x, there exists N such that for all n ≥ N, x ∈ spanningSets(μ, n).

Русский

Для каждого x существует N такое, что для всех n ≥ N выполняется x ∈ spanningSets(μ, n).

LaTeX

$$∀ x, ∃ N ∈ ℕ, ∀ n ≥ N, x ∈ spanningSets(μ, n)$$

Lean4

theorem eventually_mem_spanningSets (μ : Measure α) [SigmaFinite μ] (x : α) : ∀ᶠ n in atTop, x ∈ spanningSets μ n :=
  eventually_atTop.2 ⟨spanningSetsIndex μ x, fun _ => mem_spanningSets_of_index_le μ x⟩

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