NRR.Multivalued.Nice — nice multivalued functions

A nice multivalued function on a topological space X is represented by a single continuous scalar map on X × SignedInterval whose zero set is its graph. The sign convention is that the map is strictly negative at the left endpoint -1 and strictly positive at the right endpoint 1.

No separate set-valued topology is introduced: the multivalued function is bundled as one continuous scalar observable together with the two strict endpoint sign conditions. This module provides the evaluation projection, its continuity, extensionality reducing equality to pointwise equality, the endpoint sign lemmas, and a constructor from an unbundled continuous function.

structure NRR.NiceMV (X : Type u_2) [TopologicalSpace X] : Type u_2

A nice multivalued function on X: a continuous scalar map on X × SignedInterval that is strictly negative at the left endpoint and strictly positive at the right endpoint. Its graph is the zero set of evalMap.

• evalMap : C(X × ↑SignedInterval, ℝ)

  The bundled continuous scalar observable on X × SignedInterval.

• left_neg (x : X) : self.evalMap (x, SignedInterval.left) < 0

  The observable is strictly negative at the left endpoint -1.

• right_pos (x : X) : 0 < self.evalMap (x, SignedInterval.right)

  The observable is strictly positive at the right endpoint 1.

def NRR.NiceMV.eval {X : Type u_1} [TopologicalSpace X] (φ : NiceMV X) (x : X) (y : ↑SignedInterval) : ℝ

Evaluate a nice multivalued function at a base point and a signed-interval coordinate.

Equations

• φ.eval x y = φ.evalMap (x, y)

@[simp]

theorem NRR.NiceMV.eval_def {X : Type u_1} [TopologicalSpace X] (φ : NiceMV X) (x : X) (y : ↑SignedInterval) : φ.eval x y = φ.evalMap (x, y)

theorem NRR.NiceMV.continuous_eval {X : Type u_1} [TopologicalSpace X] (φ : NiceMV X) : Continuous fun (z : X × ↑SignedInterval) => φ.eval z.1 z.2

theorem NRR.NiceMV.continuous_eval_left {X : Type u_1} [TopologicalSpace X] (φ : NiceMV X) : Continuous fun (x : X) => φ.eval x SignedInterval.left

theorem NRR.NiceMV.continuous_eval_right {X : Type u_1} [TopologicalSpace X] (φ : NiceMV X) : Continuous fun (x : X) => φ.eval x SignedInterval.right

theorem NRR.NiceMV.eval_left_neg {X : Type u_1} [TopologicalSpace X] (φ : NiceMV X) (x : X) : φ.eval x SignedInterval.left < 0

theorem NRR.NiceMV.eval_right_pos {X : Type u_1} [TopologicalSpace X] (φ : NiceMV X) (x : X) : 0 < φ.eval x SignedInterval.right

theorem NRR.NiceMV.ext {X : Type u_1} [TopologicalSpace X] {φ ψ : NiceMV X} (h : ∀ (x : X) (y : ↑SignedInterval), φ.eval x y = ψ.eval x y) : φ = ψ

theorem NRR.NiceMV.ext_iff {X : Type u_1} [TopologicalSpace X] {φ ψ : NiceMV X} : φ = ψ ↔ ∀ (x : X) (y : ↑SignedInterval), φ.eval x y = ψ.eval x y

def NRR.NiceMV.ofFunction {X : Type u_1} [TopologicalSpace X] (f : X → ↑SignedInterval → ℝ) (hf : Continuous fun (z : X × ↑SignedInterval) => f z.1 z.2) (hleft : ∀ (x : X), f x SignedInterval.left < 0) (hright : ∀ (x : X), 0 < f x SignedInterval.right) : NiceMV X

Build a nice multivalued function from an unbundled continuous function with the required strict endpoint signs.

Equations

• NRR.NiceMV.ofFunction f hf hleft hright = { evalMap := { toFun := fun (z : X × ↑NRR.SignedInterval) => f z.1 z.2, continuous_toFun := hf }, left_neg := hleft, right_pos := hright }

theorem NRR.NiceMV.ofFunction_eval {X : Type u_1} [TopologicalSpace X] (f : X → ↑SignedInterval → ℝ) (hf : Continuous fun (z : X × ↑SignedInterval) => f z.1 z.2) (hleft : ∀ (x : X), f x SignedInterval.left < 0) (hright : ∀ (x : X), 0 < f x SignedInterval.right) (x : X) (y : ↑SignedInterval) : (ofFunction f hf hleft hright).eval x y = f x y