NRR.Multivalued.Separator.Basic — top–bottom separator structure

A top–bottom separator over a space X is a closed carrier in X × SignedInterval whose complement splits into two disjoint open regions, a lower region and an upper region, with the bottom boundary signedBottom X (points with interval coordinate -1) contained in lower and the top boundary signedTop X (points with interval coordinate 1) contained in upper.

This is the abstract separation datum used in the Akopyan–Avvakumov–Karasev prime-refinement argument. It records only the complement decomposition and the boundary placement; no signed distance function is stored, and X is not required to be compact or metric.

The elementary side API derives, from these fields, that each side lies in the carrier complement, that membership in a side excludes membership in the carrier, that a point outside the carrier lies in exactly one side, and that the two boundaries never meet the carrier.

def NRR.signedBottom (X : Type u_1) : Set (X × ↑SignedInterval)

The bottom boundary: points of X × SignedInterval whose interval coordinate is the left endpoint -1.

Equations

• NRR.signedBottom X = {z : X × ↑NRR.SignedInterval | z.2 = NRR.SignedInterval.left}

def NRR.signedTop (X : Type u_1) : Set (X × ↑SignedInterval)

The top boundary: points of X × SignedInterval whose interval coordinate is the right endpoint 1.

Equations

• NRR.signedTop X = {z : X × ↑NRR.SignedInterval | z.2 = NRR.SignedInterval.right}

structure NRR.TopBottomSeparator (X : Type u_1) [TopologicalSpace X] : Type u_1

A top–bottom separator over X: a closed carrier in X × SignedInterval whose complement is partitioned into disjoint open lower and upper regions, with the bottom boundary in lower and the top boundary in upper.

• carrier : Set (X × ↑SignedInterval)

  The closed carrier: the graph of the separating multifunction.

• isClosed_carrier : IsClosed self.carrier

  The carrier is closed.

• 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 lower and upper regions are disjoint.

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

  The complement of the carrier is 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.

theorem NRR.TopBottomSeparator.lower_subset_compl {X : Type u_1} [TopologicalSpace X] (S : TopBottomSeparator X) : S.lower ⊆ S.carrierᶜ

The lower region is contained in the carrier complement.

theorem NRR.TopBottomSeparator.upper_subset_compl {X : Type u_1} [TopologicalSpace X] (S : TopBottomSeparator X) : S.upper ⊆ S.carrierᶜ

The upper region is contained in the carrier complement.

theorem NRR.TopBottomSeparator.not_mem_carrier_of_mem_lower {X : Type u_1} [TopologicalSpace X] (S : TopBottomSeparator X) {z : X × ↑SignedInterval} (hz : z ∈ S.lower) : z ∉ S.carrier

A point of the lower region is not in the carrier.

theorem NRR.TopBottomSeparator.not_mem_carrier_of_mem_upper {X : Type u_1} [TopologicalSpace X] (S : TopBottomSeparator X) {z : X × ↑SignedInterval} (hz : z ∈ S.upper) : z ∉ S.carrier

A point of the upper region is not in the carrier.

theorem NRR.TopBottomSeparator.mem_lower_or_upper_of_not_mem {X : Type u_1} [TopologicalSpace X] (S : TopBottomSeparator X) {z : X × ↑SignedInterval} (hz : z ∉ S.carrier) : z ∈ S.lower ∨ z ∈ S.upper

A point outside the carrier lies in the lower or the upper region.

theorem NRR.TopBottomSeparator.mem_lower_iff_not_mem_upper_of_not_mem {X : Type u_1} [TopologicalSpace X] (S : TopBottomSeparator X) {z : X × ↑SignedInterval} (hz : z ∉ S.carrier) : z ∈ S.lower ↔ z ∉ S.upper

For a point outside the carrier, being in the lower region is equivalent to not being in the upper region.

theorem NRR.TopBottomSeparator.bottom_mem_lower {X : Type u_1} [TopologicalSpace X] (S : TopBottomSeparator X) (x : X) : (x, SignedInterval.left) ∈ S.lower

The bottom boundary point at x lies in the lower region.

theorem NRR.TopBottomSeparator.top_mem_upper {X : Type u_1} [TopologicalSpace X] (S : TopBottomSeparator X) (x : X) : (x, SignedInterval.right) ∈ S.upper

The top boundary point at x lies in the upper region.

theorem NRR.TopBottomSeparator.bottom_not_mem_carrier {X : Type u_1} [TopologicalSpace X] (S : TopBottomSeparator X) (x : X) : (x, SignedInterval.left) ∉ S.carrier

The bottom boundary point at x is not in the carrier.

theorem NRR.TopBottomSeparator.top_not_mem_carrier {X : Type u_1} [TopologicalSpace X] (S : TopBottomSeparator X) (x : X) : (x, SignedInterval.right) ∉ S.carrier

The top boundary point at x is not in the carrier.