Complement data for a prescribed top--bottom carrier

This module separates the closedness of a proposed carrier from the topological assertion that its complement has lower and upper components joining the two endpoint boundaries. It is useful when the carrier is obtained independently as the projection of a compact zero set: compactness proves closedness, while a cobordism or intersection-number argument supplies the complement data.

structure NRR.TopBottomComplement (X : Type u_1) [TopologicalSpace X] (carrier : Set (X × ↑SignedInterval)) : Type u_1

Complement-separation data for a prescribed carrier in X × SignedInterval.

Unlike TopBottomSeparator, closedness is not a field: it can be supplied afterwards from the construction of the carrier.

• lower : Set (X × ↑SignedInterval)

  The open lower region of the complement.

• upper : Set (X × ↑SignedInterval)

  The open upper region of the complement.

• isOpen_lower : IsOpen self.lower

  The lower region is open.

• isOpen_upper : IsOpen self.upper

  The upper region is open.

• disjoint_lower_upper : Disjoint self.lower self.upper

  The two regions are disjoint.

• compl_eq : carrierᶜ = self.lower ∪ self.upper

  The complement of the prescribed carrier is exactly the union of the two regions.

• bottom_subset_lower : signedBottom X ⊆ self.lower

  The bottom boundary lies in the lower region.

• top_subset_upper : signedTop X ⊆ self.upper

  The top boundary lies in the upper region.

def NRR.TopBottomComplement.toSeparator {X : Type u_1} [TopologicalSpace X] {carrier : Set (X × ↑SignedInterval)} (D : TopBottomComplement X carrier) (hcarrier : IsClosed carrier) : TopBottomSeparator X

Add a closedness proof to complement data, obtaining a top--bottom separator.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem NRR.TopBottomComplement.toSeparator_carrier {X : Type u_1} [TopologicalSpace X] {carrier : Set (X × ↑SignedInterval)} (D : TopBottomComplement X carrier) (hcarrier : IsClosed carrier) : (D.toSeparator hcarrier).carrier = carrier

@[simp]

theorem NRR.TopBottomComplement.toSeparator_lower {X : Type u_1} [TopologicalSpace X] {carrier : Set (X × ↑SignedInterval)} (D : TopBottomComplement X carrier) (hcarrier : IsClosed carrier) : (D.toSeparator hcarrier).lower = D.lower

@[simp]

theorem NRR.TopBottomComplement.toSeparator_upper {X : Type u_1} [TopologicalSpace X] {carrier : Set (X × ↑SignedInterval)} (D : TopBottomComplement X carrier) (hcarrier : IsClosed carrier) : (D.toSeparator hcarrier).upper = D.upper