OAI/Analysis/KadisonKastler/UltrafilterDiagonal.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A diagonal index for countably many ultrafilter-large sets

  1. theorem OAI.KadisonKastler.exists_ultrafilter_diagonal_index line 17

    Source documentation

    The index grows along the free ultrafilter, while its corresponding constraint holds at the chosen coordinate.

    theorem exists_ultrafilter_diagonal_index (ω : Ultrafilter ℕ)
    (hω : (ω : Filter ℕ) ≤ atTop) (A : ℕ → Set ℕ) (hA : ∀ n, A n ∈ ω) :
    ∃ k : ℕ → ℕ, Tendsto k (ω : Filter ℕ) atTop ∧ ∀ᶠ j in (ω : Filter ℕ), j ∈ A (k j) := by
…