Documentation

LeanPool.NandakumarRamanaRao.NRR.Multivalued.SignedInterval

NRR.Multivalued.SignedInterval — the signed interval [-1, 1] #

The signed interval is the closed real interval [-1, 1], carrying the inherited subtype topology and metric. The sign convention is that a nice multivalued observable is negative at the endpoint -1 and positive at the endpoint 1.

This module provides the endpoint elements (left, center, right), the coordinate projection coord, their coercion lemmas, compactness and connectedness of the whole interval, the ambient CompactSpace/T2Space/MetricSpace/ConnectedSpace structures, and the vertical embedding vertical used to build separator fibers.

source
@[reducible, inline]
abbrev NRR.SignedInterval :
Set ℝ

The signed interval [-1, 1] ⊆ ℝ, used as a subtype with the inherited topology and metric.

Equations
Instances For
    source
    def NRR.SignedInterval.left :
    ↑SignedInterval

    The left endpoint -1, at which a nice multivalued observable is negative.

    Equations
    Instances For
      source
      def NRR.SignedInterval.right :
      ↑SignedInterval

      The right endpoint 1, at which a nice multivalued observable is positive.

      Equations
      Instances For
        source
        def NRR.SignedInterval.center :
        ↑SignedInterval

        The center point 0.

        Equations
        Instances For
          source
          def NRR.SignedInterval.coord :
          ↑SignedInterval → ℝ

          The coordinate projection sending a signed-interval point to its underlying real number.

          Equations
          Instances For
            source
            instance NRR.SignedInterval.instNonemptyElemReal :
            Nonempty ↑SignedInterval
            source
            instance NRR.SignedInterval.instConnectedSpaceElemReal :
            ConnectedSpace ↑SignedInterval

            The signed interval is connected: it is the preconnected closed interval [-1, 1], and it is nonempty.

            source
            @[simp]
            theorem NRR.SignedInterval.coe_left :
            ↑left = -1
            source
            @[simp]
            theorem NRR.SignedInterval.coe_right :
            ↑right = 1
            source
            @[simp]
            theorem NRR.SignedInterval.coe_center :
            ↑center = 0
            source
            @[simp]
            theorem NRR.SignedInterval.coord_left :
            coord left = -1
            source
            @[simp]
            theorem NRR.SignedInterval.coord_right :
            coord right = 1
            source
            @[simp]
            theorem NRR.SignedInterval.coord_center :
            coord center = 0
            source
            theorem NRR.SignedInterval.left_ne_right :
            left ≠ right
            source
            theorem NRR.SignedInterval.right_ne_left :
            right ≠ left
            source
            theorem NRR.SignedInterval.continuous_coord :
            Continuous coord

            The coordinate projection is continuous (it is the subtype coercion).

            source
            theorem NRR.SignedInterval.compact_univ :
            IsCompact Set.univ

            The whole signed interval is compact.

            source
            theorem NRR.SignedInterval.preconnected_univ :
            IsPreconnected Set.univ

            The whole signed interval is preconnected.

            source
            theorem NRR.SignedInterval.connectedSpace :
            ConnectedSpace ↑SignedInterval

            The signed interval is a connected space.

            source
            def NRR.SignedInterval.vertical (X : Type u_1) (x : X) :
            ↑SignedInterval → X × ↑SignedInterval

            The vertical embedding y ↦ (x, y) used to build separator fibers.

            Equations
            Instances For
              source
              theorem NRR.SignedInterval.continuous_vertical {X : Type u_1} [TopologicalSpace X] (x : X) :
              Continuous (vertical X x)

              The vertical embedding is continuous.