Kuratowski–Ulam: meager sections give a meager set

isMeagre_of_isMeagre_sections: if A ⊆ X × Y has the Baire property and every vertical section {y | (x, y) ∈ A} is meager, then A is meager. This is the direction of the Kuratowski–Ulam theorem ("Fubini for Baire category", Kechris CDST 8.41) needed for the classical category route to Silver's theorem (step 3 of InfinitaryLogic/Conditional/SilverCategoryRoute.lean; see docs/silver-phase2-route.md): it makes the pullback relation on Cantor space meager once all its classes are meager.

Proof

The auxiliary direction comes first: for a nowhere dense F ⊆ X × Y (with Y second countable), residually many x have nowhere dense sections (residual_isNowhereDense_section). Indeed, taking F closed with dense open complement U, for each nonempty basic V ⊆ Y the set of x whose section of U meets V is open (projection of an open set) and dense (density of U on boxes G ×ˢ V); on the countable intersection over the basis, the section of U is dense open, so the section of F is nowhere dense. Countable unions lift this to meager M (residual_isMeagre_section).

For the main theorem, write A =ᵇ W with W open (Baire property) and let M be the (meager) symmetric difference. If A were non-meager then W is nonempty, so it contains a box G ×ˢ H; residually many x have meager M-section, and since nonempty open sets in the Baire space X are non-meager, some such x₁ lies in G. Then H ⊆ {y | (x₁, y) ∈ A} ∪ {y | (x₁, y) ∈ M} is meager, contradicting that Y is a Baire space.

theorem residual_isNowhereDense_section {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [SecondCountableTopology Y] {F : Set (X × Y)} (hF : IsNowhereDense F) : {x : X | IsNowhereDense {y : Y | (x, y) ∈ F}} ∈ residual X

For a nowhere dense subset of a product (second factor second countable), residually many vertical sections are nowhere dense.

theorem residual_isMeagre_section {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [SecondCountableTopology Y] {M : Set (X × Y)} (hM : IsMeagre M) : {x : X | IsMeagre {y : Y | (x, y) ∈ M}} ∈ residual X

For a meager subset of a product (second factor second countable), residually many vertical sections are meager.

theorem isMeagre_of_isMeagre_sections {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [SecondCountableTopology Y] [BaireSpace X] [BaireSpace Y] {A : Set (X × Y)} (hA : BaireMeasurableSet A) (hsec : ∀ (x : X), IsMeagre {y : Y | (x, y) ∈ A}) : IsMeagre A

Kuratowski–Ulam (the direction used for Silver's theorem): a set with the Baire property in a product of Baire spaces, the second factor second countable, all of whose vertical sections are meager, is meager. (Kechris, CDST 8.41.)