Theorems · Theorem · general topology

Filter.HasAntitoneBasis.subbasis_with_rel

∀ {α : Type u_3} {f : Filter α} {s : ℕ → Set α},
  f.HasAntitoneBasis s →
    ∀ {r : ℕ → ℕ → Prop},
      (∀ (m : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, r m n) →
        ∃ φ, StrictMono φ ∧ (∀ ⦃m n : ℕ⦄, m < n → r (φ m) (φ n)) ∧ f.HasAntitoneBasis (s ∘ φ)

Given an antitone basis s : ℕ → Set α of a filter, extract an antitone subbasis s ∘ φ, φ : ℕ → ℕ, such that m < n implies r (φ m) (φ n). This lemma can be used to extract an antitone basis with basis sets decreasing "sufficiently fast".

Defined in

Mathlib.Order.Filter.AtTopBot.Finite

Cited by

4 results in Mathlib

Foundations

Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound