Documentation

Mathlib.Order.Interval.Set.ProjIcc

Projection of a line onto a closed interval #

Given a linearly ordered type α, in this file we define

We also prove some trivial properties of these maps.

def Set.projIci {α : Type u_1} [LinearOrder α] (a x : α) :
(Ici a)

Projection of α to the closed interval [a, ∞).

Equations
    Instances For
      def Set.projIic {α : Type u_1} [LinearOrder α] (b x : α) :
      (Iic b)

      Projection of α to the closed interval (-∞, b].

      Equations
        Instances For
          def Set.projIcc {α : Type u_1} [LinearOrder α] (a b : α) (h : a b) (x : α) :
          (Icc a b)

          Projection of α to the closed interval [a, b].

          Equations
            Instances For
              theorem Set.coe_projIci {α : Type u_1} [LinearOrder α] (a x : α) :
              (projIci a x) = max a x
              theorem Set.coe_projIic {α : Type u_1} [LinearOrder α] (b x : α) :
              (projIic b x) = min b x
              theorem Set.coe_projIcc {α : Type u_1} [LinearOrder α] (a b : α) (h : a b) (x : α) :
              (projIcc a b h x) = max a (min b x)
              theorem Set.projIci_of_le {α : Type u_1} [LinearOrder α] {a x : α} (hx : x a) :
              projIci a x = a,
              theorem Set.projIic_of_le {α : Type u_1} [LinearOrder α] {b x : α} (hx : b x) :
              projIic b x = b,
              theorem Set.projIcc_of_le_left {α : Type u_1} [LinearOrder α] {a b : α} (h : a b) {x : α} (hx : x a) :
              projIcc a b h x = a,
              theorem Set.projIcc_of_right_le {α : Type u_1} [LinearOrder α] {a b : α} (h : a b) {x : α} (hx : b x) :
              projIcc a b h x = b,
              @[simp]
              theorem Set.projIci_self {α : Type u_1} [LinearOrder α] (a : α) :
              projIci a a = a,
              @[simp]
              theorem Set.projIic_self {α : Type u_1} [LinearOrder α] (b : α) :
              projIic b b = b,
              @[simp]
              theorem Set.projIcc_left {α : Type u_1} [LinearOrder α] {a b : α} (h : a b) :
              projIcc a b h a = a,
              @[simp]
              theorem Set.projIcc_right {α : Type u_1} [LinearOrder α] {a b : α} (h : a b) :
              projIcc a b h b = b,
              theorem Set.projIci_eq_self {α : Type u_1} [LinearOrder α] {a x : α} :
              projIci a x = a, x a
              theorem Set.projIic_eq_self {α : Type u_1} [LinearOrder α] {b x : α} :
              projIic b x = b, b x
              theorem Set.projIcc_eq_left {α : Type u_1} [LinearOrder α] {a b x : α} (h : a < b) :
              projIcc a b x = a, x a
              theorem Set.projIcc_eq_right {α : Type u_1} [LinearOrder α] {a b x : α} (h : a < b) :
              projIcc a b x = b, b x
              theorem Set.projIci_of_mem {α : Type u_1} [LinearOrder α] {a x : α} (hx : x Ici a) :
              projIci a x = x, hx
              theorem Set.projIic_of_mem {α : Type u_1} [LinearOrder α] {b x : α} (hx : x Iic b) :
              projIic b x = x, hx
              theorem Set.projIcc_of_mem {α : Type u_1} [LinearOrder α] {a b : α} (h : a b) {x : α} (hx : x Icc a b) :
              projIcc a b h x = x, hx
              @[simp]
              theorem Set.projIci_coe {α : Type u_1} [LinearOrder α] {a : α} (x : (Ici a)) :
              projIci a x = x
              @[simp]
              theorem Set.projIic_coe {α : Type u_1} [LinearOrder α] {b : α} (x : (Iic b)) :
              projIic b x = x
              @[simp]
              theorem Set.projIcc_val {α : Type u_1} [LinearOrder α] {a b : α} (h : a b) (x : (Icc a b)) :
              projIcc a b h x = x
              theorem Set.projIci_surjOn {α : Type u_1} [LinearOrder α] {a : α} :
              theorem Set.projIic_surjOn {α : Type u_1} [LinearOrder α] {b : α} :
              theorem Set.projIcc_surjOn {α : Type u_1} [LinearOrder α] {a b : α} (h : a b) :
              SurjOn (projIcc a b h) (Icc a b) univ
              theorem Set.projIcc_surjective {α : Type u_1} [LinearOrder α] {a b : α} (h : a b) :
              @[simp]
              theorem Set.range_projIci {α : Type u_1} [LinearOrder α] {a : α} :
              @[simp]
              theorem Set.range_projIic {α : Type u_1} [LinearOrder α] {a : α} :
              @[simp]
              theorem Set.range_projIcc {α : Type u_1} [LinearOrder α] {a b : α} (h : a b) :
              theorem Set.monotone_projIci {α : Type u_1} [LinearOrder α] {a : α} :
              theorem Set.monotone_projIic {α : Type u_1} [LinearOrder α] {a : α} :
              theorem Set.monotone_projIcc {α : Type u_1} [LinearOrder α] {a b : α} (h : a b) :
              theorem Set.strictMonoOn_projIci {α : Type u_1} [LinearOrder α] {a : α} :
              theorem Set.strictMonoOn_projIic {α : Type u_1} [LinearOrder α] {b : α} :
              theorem Set.strictMonoOn_projIcc {α : Type u_1} [LinearOrder α] {a b : α} (h : a b) :
              StrictMonoOn (projIcc a b h) (Icc a b)
              def Set.IciExtend {α : Type u_1} {β : Type u_2} [LinearOrder α] {a : α} (f : (Ici a)β) :
              αβ

              Extend a function [a, ∞) → β to a map α → β.

              Equations
                Instances For
                  def Set.IicExtend {α : Type u_1} {β : Type u_2} [LinearOrder α] {b : α} (f : (Iic b)β) :
                  αβ

                  Extend a function (-∞, b] → β to a map α → β.

                  Equations
                    Instances For
                      def Set.IccExtend {α : Type u_1} {β : Type u_2} [LinearOrder α] {a b : α} (h : a b) (f : (Icc a b)β) :
                      αβ

                      Extend a function [a, b] → β to a map α → β.

                      Equations
                        Instances For
                          theorem Set.IciExtend_apply {α : Type u_1} {β : Type u_2} [LinearOrder α] {a : α} (f : (Ici a)β) (x : α) :
                          IciExtend f x = f max a x,
                          theorem Set.IicExtend_apply {α : Type u_1} {β : Type u_2} [LinearOrder α] {b : α} (f : (Iic b)β) (x : α) :
                          IicExtend f x = f min b x,
                          theorem Set.IccExtend_apply {α : Type u_1} {β : Type u_2} [LinearOrder α] {a b : α} (h : a b) (f : (Icc a b)β) (x : α) :
                          IccExtend h f x = f max a (min b x),
                          @[simp]
                          theorem Set.range_IciExtend {α : Type u_1} {β : Type u_2} [LinearOrder α] {a : α} (f : (Ici a)β) :
                          @[simp]
                          theorem Set.range_IicExtend {α : Type u_1} {β : Type u_2} [LinearOrder α] {b : α} (f : (Iic b)β) :
                          @[simp]
                          theorem Set.IccExtend_range {α : Type u_1} {β : Type u_2} [LinearOrder α] {a b : α} (h : a b) (f : (Icc a b)β) :
                          theorem Set.IciExtend_of_le {α : Type u_1} {β : Type u_2} [LinearOrder α] {a x : α} (f : (Ici a)β) (hx : x a) :
                          IciExtend f x = f a,
                          theorem Set.IicExtend_of_le {α : Type u_1} {β : Type u_2} [LinearOrder α] {b x : α} (f : (Iic b)β) (hx : b x) :
                          IicExtend f x = f b,
                          theorem Set.IccExtend_of_le_left {α : Type u_1} {β : Type u_2} [LinearOrder α] {a b : α} (h : a b) {x : α} (f : (Icc a b)β) (hx : x a) :
                          IccExtend h f x = f a,
                          theorem Set.IccExtend_of_right_le {α : Type u_1} {β : Type u_2} [LinearOrder α] {a b : α} (h : a b) {x : α} (f : (Icc a b)β) (hx : b x) :
                          IccExtend h f x = f b,
                          @[simp]
                          theorem Set.IciExtend_self {α : Type u_1} {β : Type u_2} [LinearOrder α] {a : α} (f : (Ici a)β) :
                          IciExtend f a = f a,
                          @[simp]
                          theorem Set.IicExtend_self {α : Type u_1} {β : Type u_2} [LinearOrder α] {b : α} (f : (Iic b)β) :
                          IicExtend f b = f b,
                          @[simp]
                          theorem Set.IccExtend_left {α : Type u_1} {β : Type u_2} [LinearOrder α] {a b : α} (h : a b) (f : (Icc a b)β) :
                          IccExtend h f a = f a,
                          @[simp]
                          theorem Set.IccExtend_right {α : Type u_1} {β : Type u_2} [LinearOrder α] {a b : α} (h : a b) (f : (Icc a b)β) :
                          IccExtend h f b = f b,
                          theorem Set.IciExtend_of_mem {α : Type u_1} {β : Type u_2} [LinearOrder α] {a x : α} (f : (Ici a)β) (hx : x Ici a) :
                          IciExtend f x = f x, hx
                          theorem Set.IicExtend_of_mem {α : Type u_1} {β : Type u_2} [LinearOrder α] {b x : α} (f : (Iic b)β) (hx : x Iic b) :
                          IicExtend f x = f x, hx
                          theorem Set.IccExtend_of_mem {α : Type u_1} {β : Type u_2} [LinearOrder α] {a b : α} (h : a b) {x : α} (f : (Icc a b)β) (hx : x Icc a b) :
                          IccExtend h f x = f x, hx
                          @[simp]
                          theorem Set.IciExtend_coe {α : Type u_1} {β : Type u_2} [LinearOrder α] {a : α} (f : (Ici a)β) (x : (Ici a)) :
                          IciExtend f x = f x
                          @[simp]
                          theorem Set.IicExtend_coe {α : Type u_1} {β : Type u_2} [LinearOrder α] {b : α} (f : (Iic b)β) (x : (Iic b)) :
                          IicExtend f x = f x
                          @[simp]
                          theorem Set.IccExtend_val {α : Type u_1} {β : Type u_2} [LinearOrder α] {a b : α} (h : a b) (f : (Icc a b)β) (x : (Icc a b)) :
                          IccExtend h f x = f x
                          theorem Set.IccExtend_eq_self {α : Type u_1} {β : Type u_2} [LinearOrder α] {a b : α} (h : a b) (f : αβ) (ha : x < a, f x = f a) (hb : ∀ (x : α), b < xf x = f b) :

                          If f : α → β is a constant both on $(-∞, a]$ and on $[b, +∞)$, then the extension of this function from $[a, b]$ to the whole line is equal to the original function.

                          theorem Monotone.IciExtend {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {a : α} {f : (Set.Ici a)β} (hf : Monotone f) :
                          theorem Monotone.IicExtend {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {b : α} {f : (Set.Iic b)β} (hf : Monotone f) :
                          theorem Monotone.IccExtend {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {a b : α} (h : a b) {f : (Set.Icc a b)β} (hf : Monotone f) :
                          theorem StrictMono.strictMonoOn_IciExtend {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {a : α} {f : (Set.Ici a)β} (hf : StrictMono f) :
                          theorem StrictMono.strictMonoOn_IicExtend {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {b : α} {f : (Set.Iic b)β} (hf : StrictMono f) :
                          theorem StrictMono.strictMonoOn_IccExtend {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {a b : α} (h : a b) {f : (Set.Icc a b)β} (hf : StrictMono f) :
                          theorem Set.OrdConnected.IciExtend {α : Type u_1} [LinearOrder α] {a : α} {s : Set (Ici a)} (hs : s.OrdConnected) :
                          {x : α | IciExtend (fun (x : (Ici a)) => x s) x}.OrdConnected
                          theorem Set.OrdConnected.IicExtend {α : Type u_1} [LinearOrder α] {b : α} {s : Set (Iic b)} (hs : s.OrdConnected) :
                          {x : α | IicExtend (fun (x : (Iic b)) => x s) x}.OrdConnected
                          theorem Set.OrdConnected.restrict {α : Type u_1} [LinearOrder α] {s t : Set α} (hs : s.OrdConnected) :
                          {x : t | t.restrict (fun (x : α) => x s) x}.OrdConnected