NRR.Multivalued.Separator.ToNiceMV — separators as nice multivalued functions

Every top–bottom separator S over a nonempty metric base X gives a nice multivalued function S.toNiceMV, whose scalar observable is the signed distance to the carrier. Its zero set is exactly the carrier: the graph of the separating multifunction is recovered as the zero set of a single continuous scalar function, with the required strict endpoint signs coming from the signed distance being negative at the bottom boundary and positive at the top boundary.

Separators also pull back along a continuous base map f : Y → X through the product map (y, t) ↦ (f y, t): carrier, lower, and upper regions are pulled back by preimage, which preserves closedness, openness, disjointness, complements, and the boundary placement. The pulled-back separator's nice multivalued function has the same zero set as the pullback of the original nice multivalued function, even though the two signed distances are computed in different product metrics and need not agree pointwise.

noncomputable def NRR.TopBottomSeparator.toNiceMV {X : Type u_1} [MetricSpace X] [Nonempty X] (S : TopBottomSeparator X) : NiceMV X

The nice multivalued function attached to a top–bottom separator: its scalar observable is the signed distance to the carrier, so its zero set is exactly the carrier.

Equations

• S.toNiceMV = { evalMap := S.signedDistanceMap, left_neg := ⋯, right_pos := ⋯ }

theorem NRR.TopBottomSeparator.toNiceMV_eval {X : Type u_1} [MetricSpace X] [Nonempty X] (S : TopBottomSeparator X) (x : X) (t : ↑SignedInterval) : S.toNiceMV.eval x t = S.signedDistance (x, t)

theorem NRR.TopBottomSeparator.zero_toNiceMV_iff {X : Type u_1} [MetricSpace X] [Nonempty X] (S : TopBottomSeparator X) (x : X) (t : ↑SignedInterval) : S.toNiceMV.Zero x t ↔ (x, t) ∈ S.carrier

theorem NRR.TopBottomSeparator.zeroSet_toNiceMV {X : Type u_1} [MetricSpace X] [Nonempty X] (S : TopBottomSeparator X) : S.toNiceMV.zeroSet = S.carrier

def NRR.TopBottomSeparator.pullback {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (S : TopBottomSeparator X) (f : C(Y, X)) : TopBottomSeparator Y

Pull back a top–bottom separator S on X along a continuous base map f : Y → X through the product map (y, t) ↦ (f y, t). Carrier, lower, and upper regions are pulled back by preimage.

Equations

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

theorem NRR.TopBottomSeparator.pullback_carrier {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (S : TopBottomSeparator X) (f : C(Y, X)) : (S.pullback f).carrier = (fun (z : Y × ↑SignedInterval) => (f z.1, z.2)) ⁻¹' S.carrier

theorem NRR.TopBottomSeparator.pullback_toNiceMV_zeroSet {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] [Nonempty X] [Nonempty Y] (S : TopBottomSeparator X) (f : C(Y, X)) : (S.pullback f).toNiceMV.zeroSet = (S.toNiceMV.pullback f).zeroSet