The Kuratowski–Ulam theorem

The Kuratowski–Ulam theorem is the analogue of Fubini's theorem for Baire category: a set s with the Baire property in a product X × Y with Y second countable is comeagre if and only if, for comeagrely many x, its section {y | (x, y) ∈ s} is comeagre. Equivalently, s is meagre if and only if comeagrely many of its sections are meagre. No Baire hypothesis on the factors and no countability hypothesis on X is needed; exchanging the order of the two quantifiers uses second countability of both factors.

The sections of s : Set (X × Y) are written (x, ·) ⁻¹' s and (·, y) ⁻¹' s. The curried filter (residual X).curry (residual Y) is the filter of sets with comeagrely many comeagre sections, so the theorem says that this filter agrees with residual (X × Y) on sets with the Baire property; one inclusion holds for all sets.

This is how meagreness of a relation is checked through its sections, for example to show that an equivalence relation with the Baire property and meagre classes is meagre in the square.

Main results

• Dense.eventually_dense_curry_left: comeagrely many sections of a dense open set are dense.
• IsNowhereDense.eventually_isNowhereDense_curry_left: comeagrely many sections of a nowhere dense set are nowhere dense.
• TauCeti.curry_le_residual: (residual X).curry (residual Y) ≤ residual (X × Y), that is, a comeagre subset of X × Y has comeagre sections over a comeagre set of x.
• IsMeagre.eventually_isMeagre_curry_left, IsMeagre.eventually_isMeagre_curry_right: comeagrely many sections of a meagre set are meagre.
• IsMeagre.prod_left, IsMeagre.prod_right: a product with a meagre factor is meagre.
• BaireMeasurableSet.baireMeasurableSet_curry_left: comeagrely many sections of a set with the Baire property have the Baire property.
• BaireMeasurableSet.eventually_eventually_left_iff_mem_residual: the Kuratowski–Ulam theorem, with the right-hand form eventually_eventually_right_iff_mem_residual and the exchange of quantifiers eventually_eventually_swap.
• BaireMeasurableSet.eventually_isMeagre_curry_left_iff_isMeagre, BaireMeasurableSet.isMeagre_of_forall_isMeagre_curry_left and their right-hand forms eventually_isMeagre_curry_right_iff_isMeagre, isMeagre_of_forall_isMeagre_curry_right: the meagre-sections forms.

References

• K. Kuratowski and S. Ulam, Quelques propriétés topologiques du produit combinatoire, Fundamenta Mathematicae 19 (1932), 247–251.
• A. S. Kechris, Classical Descriptive Set Theory, Springer, 1995, Theorem 8.41.
• The statements and the proof of the converse direction follow Mathlib PR #17368 by Felix Weilacher (curry_le_residual, IsMeagre.prod_left, and the BaireMeasurableSet forms of the theorem).

theorem Dense.eventually_dense_curry_left {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [SecondCountableTopology Y] {s : Set (X × Y)} (hd : Dense s) (ho : IsOpen s) : ∀ᶠ (x : X) in residual X, Dense ((fun (x_1 : Y) => (x, x_1)) ⁻¹' s)

If s is a dense open subset of X × Y with Y second countable, then for comeagrely many x the section (x, ·) ⁻¹' s is dense.

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

If s is a nowhere dense subset of X × Y with Y second countable, then for comeagrely many x the section (x, ·) ⁻¹' s is nowhere dense.

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

One 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.

theorem TauCeti.eventually_eventually_left_of_mem_residual {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. If Y is second countable and s is comeagre in X × Y, then comeagrely many sections (x, ·) ⁻¹' s are comeagre.

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

If Y is second countable and s is meagre in X × Y, then comeagrely many sections (x, ·) ⁻¹' s are meagre.

theorem BaireMeasurableSet.baireMeasurableSet_curry_left {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, BaireMeasurableSet ((fun (x_1 : Y) => (x, x_1)) ⁻¹' s)

If Y is second countable and s has the Baire property in X × Y, then comeagrely many sections (x, ·) ⁻¹' s have the Baire property.

theorem TauCeti.eventually_eventually_right_of_mem_residual {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

One half of the Kuratowski–Ulam theorem. If X is second countable and s is comeagre in X × Y, then comeagrely many sections (·, y) ⁻¹' s are comeagre.

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

If X is second countable and s is meagre in X × Y, then comeagrely many sections (·, y) ⁻¹' s are meagre.

theorem IsMeagre.prod_left {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} (hs : IsMeagre s) (t : Set Y) : IsMeagre (s ×ˢ t)

A product whose left factor is meagre is meagre.

theorem IsMeagre.prod_right {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {t : Set Y} (ht : IsMeagre t) (s : Set X) : IsMeagre (s ×ˢ t)

A product whose right factor is meagre is meagre.

theorem BaireMeasurableSet.baireMeasurableSet_curry_right {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, BaireMeasurableSet ((fun (x : X) => (x, y)) ⁻¹' s)

If X is second countable and s has the Baire property in X × Y, then comeagrely many sections (·, y) ⁻¹' s have the Baire property.

theorem BaireMeasurableSet.frequently_curry_of_not_isMeagre {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [SecondCountableTopology Y] {s : Set (X × Y)} (hs : BaireMeasurableSet s) (hn : ¬IsMeagre s) : ∃ᶠ (p : X × Y) in (residual X).curry (residual Y), p ∈ s

If Y is second countable, a non-meagre set s with the Baire property in X × Y is frequently met along the curried residual filter: the set of x whose section (x, ·) ⁻¹' s is non-meagre is itself non-meagre.

theorem BaireMeasurableSet.eventually_eventually_left_iff_mem_residual {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)

The 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).

theorem BaireMeasurableSet.eventually_isMeagre_curry_left_iff_isMeagre {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 : Y) => (x, x_1)) ⁻¹' s)) ↔ IsMeagre s

The Kuratowski–Ulam theorem, meagre form. If Y is second countable, a set s with the Baire property in X × Y is meagre if and only if comeagrely many sections (x, ·) ⁻¹' s are meagre.

theorem BaireMeasurableSet.isMeagre_of_forall_isMeagre_curry_left {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [SecondCountableTopology Y] {s : Set (X × Y)} (hs : BaireMeasurableSet s) (h : ∀ (x : X), IsMeagre ((fun (x_1 : Y) => (x, x_1)) ⁻¹' s)) : IsMeagre s

If Y is second countable, a set with the Baire property in X × Y all of whose sections (x, ·) ⁻¹' s are meagre is meagre.

theorem BaireMeasurableSet.eventually_eventually_right_iff_mem_residual {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, right-hand form. If X is second countable, a set s with the Baire property in X × Y is comeagre if and only if comeagrely many sections (·, y) ⁻¹' s are comeagre.

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

For a set with the Baire property in a product of second countable spaces, the two orders of the category quantifiers agree.

theorem BaireMeasurableSet.eventually_isMeagre_curry_right_iff_isMeagre {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) => (x, y)) ⁻¹' s)) ↔ IsMeagre s

The Kuratowski–Ulam theorem, right-hand meagre form. If X is second countable, a set s with the Baire property in X × Y is meagre if and only if comeagrely many sections (·, y) ⁻¹' s are meagre.

theorem BaireMeasurableSet.isMeagre_of_forall_isMeagre_curry_right {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [SecondCountableTopology X] {s : Set (X × Y)} (hs : BaireMeasurableSet s) (h : ∀ (y : Y), IsMeagre ((fun (x : X) => (x, y)) ⁻¹' s)) : IsMeagre s

If X is second countable, a set with the Baire property in X × Y all of whose sections (·, y) ⁻¹' s are meagre is meagre.