NRR.Multivalued.Separator.Fibers — vertical fibers meet the carrier

Every vertical interval {x} × SignedInterval meets the carrier of a top–bottom separator. The argument is a pure connectedness fact: if the vertical fiber avoided the carrier, then the two disjoint open regions lower and upper would pull back along the vertical embedding to a separation of the connected signed interval, with the bottom endpoint on the lower side and the top endpoint on the upper side. This contradicts connectedness of SignedInterval.

Consequences: each vertical fiber is nonempty, the carrier is nonempty whenever X is nonempty, and the vertical path through any point meets the carrier. Nonemptiness of the carrier is therefore derived rather than assumed, so no separate nonemptiness field is needed.

theorem NRR.connected_univ_not_open_separation {Y : Type u_1} [TopologicalSpace Y] [ConnectedSpace Y] {L U : Set Y} (hL : IsOpen L) (hU : IsOpen U) (hdisj : Disjoint L U) (hcover : L ∪ U = Set.univ) {l u : Y} (hl : l ∈ L) (hu : u ∈ U) : False

A connected space cannot be covered by two disjoint nonempty open sets.

theorem NRR.TopBottomSeparator.exists_mem_fiber {X : Type u_1} [TopologicalSpace X] (S : TopBottomSeparator X) (x : X) : ∃ (y : ↑SignedInterval), (x, y) ∈ S.carrier

Every vertical fiber over x meets the carrier of the separator.

theorem NRR.TopBottomSeparator.fiber_nonempty {X : Type u_1} [TopologicalSpace X] (S : TopBottomSeparator X) (x : X) : {y : ↑SignedInterval | (x, y) ∈ S.carrier}.Nonempty

The vertical fiber over x is nonempty.

theorem NRR.TopBottomSeparator.carrier_nonempty {X : Type u_1} [TopologicalSpace X] [Nonempty X] (S : TopBottomSeparator X) : S.carrier.Nonempty

The carrier is nonempty whenever X is nonempty.

theorem NRR.TopBottomSeparator.vertical_path_intersects {X : Type u_1} [TopologicalSpace X] (S : TopBottomSeparator X) (x : X) : (Set.range (SignedInterval.vertical X x) ∩ S.carrier).Nonempty

The vertical path through x meets the carrier.