Preconnected sets in a product with preconnected fibres

A subset of X × Y need not be preconnected even when every vertical fibre is: the fibres may fail to be linked to one another. They are linked as soon as the set contains a preconnected set meeting every nonempty fibre, for instance the graph of a continuous map over a preconnected base. This is how one shows that the regions between continuous graphs over a connected base, such as the sectors of a cylindrical stack, are connected.

Main declarations

• TauCeti.isPreconnected_of_isPreconnected_preimage_prodMk: a set with preconnected fibres containing a preconnected set that meets each of its nonempty fibres is preconnected.
• TauCeti.isPreconnected_of_isPreconnected_preimage_prodMk_of_continuous: a set with preconnected fibres containing the graph of a continuous map over a preconnected base is preconnected.

theorem TauCeti.isPreconnected_of_isPreconnected_preimage_prodMk {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s t : Set (X × Y)} (ht : IsPreconnected t) (hts : t ⊆ s) (hst : Prod.fst '' s ⊆ Prod.fst '' t) (hs : ∀ (x : X), IsPreconnected (Prod.mk x ⁻¹' s)) : IsPreconnected s

A set s ⊆ X × Y is preconnected if each of its fibres {y | (x, y) ∈ s} is preconnected and it contains a preconnected set t meeting every nonempty fibre of s.

theorem TauCeti.isPreconnected_of_isPreconnected_preimage_prodMk_of_continuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [PreconnectedSpace X] {s : Set (X × Y)} {f : X → Y} (hf : Continuous f) (hfs : ∀ (x : X), (x, f x) ∈ s) (hs : ∀ (x : X), IsPreconnected (Prod.mk x ⁻¹' s)) : IsPreconnected s

Over a preconnected base, a set s ⊆ X × Y is preconnected if each of its fibres {y | (x, y) ∈ s} is preconnected and it contains the graph of a continuous map f : X → Y.