Documentation

LeanPool.RearrangementNumber.NonMRR.Category

The uniformity of the meagre ideal #

The definition nonM below uses the usual topology on the real numbers. In particular it does not define this cardinal by means of slaloms.

This file also proves the elementary countable-family slalom avoidance lemma. The category comparison used in the final proof is developed in NonMRR.CategoryBound; the general Bartoszyński characterization is not assumed.

source
noncomputable def NonMRR.nonMeagreCardinal (X : Type u) [TopologicalSpace X] :
Cardinal.{u}

The least size of a nonmeagre subset of a topological space.

Equations
Instances For
    source
    noncomputable def NonMRR.nonM :
    Cardinal.{0}

    The uniformity of the meagre ideal on the real line, as in the manuscript.

    Equations
    Instances For
      source
      noncomputable def NonMRR.nonMBaire :
      Cardinal.{0}

      The corresponding cardinal for Baire space; no identification is postulated.

      Equations
      Instances For
        source
        theorem NonMRR.nonMeagreCardinal_le_mk {X : Type u} [TopologicalSpace X] {s : Set X} (hs : ¬IsMeagre s) :
        nonMeagreCardinal X ≤ Cardinal.mk ↑s
        source
        theorem NonMRR.isMeagre_of_mk_lt_nonMeagreCardinal {X : Type u} [TopologicalSpace X] {s : Set X} (hs : Cardinal.mk ↑s < nonMeagreCardinal X) :
        IsMeagre s

        Every set smaller than the uniformity of the meagre ideal is meagre.

        source
        theorem NonMRR.isMeagre_of_mk_lt_nonM {s : Set ℝ} (hs : Cardinal.mk ↑s < nonM) :
        IsMeagre s
        source
        theorem NonMRR.exists_nonmeagre_minimizer (X : Type u) [TopologicalSpace X] [BaireSpace X] [Nonempty X] :
        ∃ (s : Set X), ¬IsMeagre s ∧ Cardinal.mk ↑s = nonMeagreCardinal X

        In a nonempty Baire space, the defining minimum has an actual witness.

        source
        theorem NonMRR.nonMeagreCardinal_le_mk_space (X : Type u) [TopologicalSpace X] [BaireSpace X] [Nonempty X] :
        nonMeagreCardinal X ≤ Cardinal.mk X
        source
        theorem NonMRR.isMeagre_of_countable {X : Type u} [TopologicalSpace X] [T1Space X] [PerfectSpace X] {s : Set X} (hs : s.Countable) :
        IsMeagre s

        Countable sets are meagre in a perfect T₁ space.

        source
        theorem NonMRR.aleph0_lt_nonM :
        Cardinal.aleph0 < nonM

        The real uniformity is strictly larger than the countable cardinal.

        source
        theorem NonMRR.exists_eventually_avoids_of_countable {Φ : Set (ℕ → Finset ℕ)} (hΦ : Φ.Countable) :
        ∃ (x : ℕ → ℕ), ∀ φ ∈ Φ, ∀ᶠ (n : ℕ) in Filter.atTop, x n ∉ φ n

        A countable collection of finite slaloms has a common eventual avoider. No uniform width bound is needed for this elementary diagonal argument.

        source
        theorem NonMRR.isMeagre_eventually_ne (x : ℕ → ℕ) :
        IsMeagre {f : ℕ → ℕ | ∀ᶠ (n : ℕ) in Filter.atTop, f n ≠ x n}

        Eventual disagreement with a fixed function is a meagre condition in Baire space.

        source
        theorem NonMRR.exists_frequently_eq_of_not_isMeagre {s : Set (ℕ → ℕ)} (hs : ¬IsMeagre s) (x : ℕ → ℕ) :
        ∃ f ∈ s, ∃ᶠ (n : ℕ) in Filter.atTop, f n = x n

        Every nonmeagre family in Baire space agrees infinitely often with each prescribed function somewhere in the family.