Baire

Results named in Tau Ceti's TauCeti.Topology.Baire modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremThe Kuratowski–Ulam theorem#

If Y is second countable, a set s with the Baire property in X × Y is comeagre if and only if comeagrely many sections (x, ·) ⁻¹' s are comeagre, that is, if and only if it belongs to the curried residual filter (residual X).curry (residual Y).

BaireMeasurableSet.eventually_eventually_left_iff_mem_residual.{u_1, u_2} {X : Type u_1}
  {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [SecondCountableTopology Y]
  {s : Set (X × Y)} (hs : BaireMeasurableSet s) :
  (∀ᶠ (x : X) in residual X, ∀ᶠ (y : Y) in residual Y, (x, y) ∈ s) ↔ s ∈ residual (X × Y)

Lean

Formalized in Tau Ceti as BaireMeasurableSet.eventually_eventually_left_iff_mem_residual.

Other forms

The Kuratowski–Ulam theorem, right-hand form. Formalized in Tau Ceti as BaireMeasurableSet.eventually_eventually_right_iff_mem_residual.

BaireMeasurableSet.eventually_eventually_right_iff_mem_residual.{u_1, u_2} {X : Type u_1}
  {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [SecondCountableTopology X]
  {s : Set (X × Y)} (hs : BaireMeasurableSet s) :
  (∀ᶠ (y : Y) in residual Y, ∀ᶠ (x : X) in residual X, (x, y) ∈ s) ↔ s ∈ residual (X × Y)

The Kuratowski–Ulam theorem, meagre form. Formalized in Tau Ceti as BaireMeasurableSet.eventually_isMeagre_curry_left_iff_isMeagre.

BaireMeasurableSet.eventually_isMeagre_curry_left_iff_isMeagre.{u_1, u_2} {X : Type u_1}
  {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [SecondCountableTopology Y]
  {s : Set (X × Y)} (hs : BaireMeasurableSet s) :
  (∀ᶠ (x : X) in residual X, IsMeagre ((fun x_1 => (x, x_1)) ⁻¹' s)) ↔ IsMeagre s

The Kuratowski–Ulam theorem, right-hand meagre form. Formalized in Tau Ceti as BaireMeasurableSet.eventually_isMeagre_curry_right_iff_isMeagre.

BaireMeasurableSet.eventually_isMeagre_curry_right_iff_isMeagre.{u_1, u_2} {X : Type u_1}
  {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [SecondCountableTopology X]
  {s : Set (X × Y)} (hs : BaireMeasurableSet s) :
  (∀ᶠ (y : Y) in residual Y, IsMeagre ((fun x => (x, y)) ⁻¹' s)) ↔ IsMeagre s

Sources

• Tau Ceti documentation: BaireMeasurableSet.eventually_eventually_left_iff_mem_residual
• Source of BaireMeasurableSet.eventually_eventually_left_iff_mem_residual in TauCeti/Topology/Baire/KuratowskiUlam.lean

LeanBaireMeasurableSet.eventually_eventually_left_iff_mem_residual · BaireMeasurableSet.eventually_eventually_right_iff_mem_residual · BaireMeasurableSet.eventually_isMeagre_curry_left_iff_isMeagre · BaireMeasurableSet.eventually_isMeagre_curry_right_iff_isMeagre

Uses 1 · Used by 1

Proof usesOne half of the Kuratowski–Ulam theorem

Used byThe category route to Silver's theorem

TheoremMycielski's theorem#

Let X be a nonempty perfect completely metrizable space, for example a nonempty perfect Polish space, and let R n be a meagre set of k n-tuples of points of X for each n. There is a continuous injection f of Cantor space into X such that for every n and every injective tuple a of k n points of Cantor space, f ∘ a ∉ R n.

TauCeti.mycielski.{u_1} {X : Type u_1} [TopologicalSpace X]
  [TopologicalSpace.IsCompletelyMetrizableSpace X] [PerfectSpace X] [Nonempty X] (k : ℕ → ℕ)
  (R : (n : ℕ) → Set (Fin (k n) → X)) (hR : ∀ (n : ℕ), IsMeagre (R n)) :
  ∃ f,
    Continuous f ∧
      Function.Injective f ∧
        ∀ (n : ℕ) (a : Fin (k n) → ℕ → Bool), Function.Injective a → f ∘ a ∉ R n

Lean

Formalized in Tau Ceti as TauCeti.mycielski.

Other forms

Mycielski's theorem, binary case. Formalized in Tau Ceti as TauCeti.mycielski_prod.

TauCeti.mycielski_prod.{u_1} {X : Type u_1} [TopologicalSpace X]
  [TopologicalSpace.IsCompletelyMetrizableSpace X] [PerfectSpace X] [Nonempty X] {M : Set (X × X)}
  (hM : IsMeagre M) :
  ∃ f, Continuous f ∧ Function.Injective f ∧ ∀ (x y : ℕ → Bool), x ≠ y → (f x, f y) ∉ M

Sources

• Tau Ceti documentation: TauCeti.mycielski
• Source of TauCeti.mycielski in TauCeti/Topology/Baire/Mycielski.lean

LeanTauCeti.mycielski · TauCeti.mycielski_prod

Used by 1

Used byThe category route to Silver's theorem

TheoremOne half of the Kuratowski–Ulam theorem#

If Y is second countable, every comeagre subset of X × Y has comeagre sections (x, ·) ⁻¹' s over a comeagre set of x.

TauCeti.curry_le_residual.{u_1, u_2} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X]
  [TopologicalSpace Y] [SecondCountableTopology Y] :
  (residual X).curry (residual Y) ≤ residual (X × Y)

Lean

Formalized in Tau Ceti as TauCeti.curry_le_residual.

Other forms

One half of the Kuratowski–Ulam theorem. Formalized in Tau Ceti as TauCeti.eventually_eventually_left_of_mem_residual.

TauCeti.eventually_eventually_left_of_mem_residual.{u_1, u_2} {X : Type u_1} {Y : Type u_2}
  [TopologicalSpace X] [TopologicalSpace Y] [SecondCountableTopology Y] {s : Set (X × Y)}
  (hs : s ∈ residual (X × Y)) : ∀ᶠ (x : X) in residual X, ∀ᶠ (y : Y) in residual Y, (x, y) ∈ s

One half of the Kuratowski–Ulam theorem. Formalized in Tau Ceti as TauCeti.eventually_eventually_right_of_mem_residual.

TauCeti.eventually_eventually_right_of_mem_residual.{u_1, u_2} {X : Type u_1} {Y : Type u_2}
  [TopologicalSpace X] [TopologicalSpace Y] [SecondCountableTopology X] {s : Set (X × Y)}
  (hs : s ∈ residual (X × Y)) : ∀ᶠ (y : Y) in residual Y, ∀ᶠ (x : X) in residual X, (x, y) ∈ s

Sources

• Tau Ceti documentation: TauCeti.curry_le_residual
• Source of TauCeti.curry_le_residual in TauCeti/Topology/Baire/KuratowskiUlam.lean

LeanTauCeti.curry_le_residual · TauCeti.eventually_eventually_left_of_mem_residual · TauCeti.eventually_eventually_right_of_mem_residual

Used by 1

Used byThe Kuratowski–Ulam theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.