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 : α) :
(Set.Ici a)

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

Equations
Instances For
    def Set.projIic {α : Type u_1} [LinearOrder α] (b : α) (x : α) :
    (Set.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 : α) :
      (Set.Icc a b)

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

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

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

        Equations
        Instances For
          def Set.IicExtend {α : Type u_1} {β : Type u_2} [LinearOrder α] {b : α} (f : (Set.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 : (Set.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 : (Set.Ici a)β) (x : α) :
              Set.IciExtend f x = f max a x,
              theorem Set.IicExtend_apply {α : Type u_1} {β : Type u_2} [LinearOrder α] {b : α} (f : (Set.Iic b)β) (x : α) :
              Set.IicExtend f x = f min b x,
              theorem Set.IccExtend_apply {α : Type u_1} {β : Type u_2} [LinearOrder α] {a : α} {b : α} (h : a b) (f : (Set.Icc a b)β) (x : α) :
              Set.IccExtend h f x = f max a (min b x),
              @[simp]
              theorem Set.range_IciExtend {α : Type u_1} {β : Type u_2} [LinearOrder α] {a : α} (f : (Set.Ici a)β) :
              @[simp]
              theorem Set.range_IicExtend {α : Type u_1} {β : Type u_2} [LinearOrder α] {b : α} (f : (Set.Iic b)β) :
              @[simp]
              theorem Set.IccExtend_range {α : Type u_1} {β : Type u_2} [LinearOrder α] {a : α} {b : α} (h : a b) (f : (Set.Icc a b)β) :
              theorem Set.IciExtend_of_le {α : Type u_1} {β : Type u_2} [LinearOrder α] {a : α} {x : α} (f : (Set.Ici a)β) (hx : x a) :
              Set.IciExtend f x = f a,
              theorem Set.IicExtend_of_le {α : Type u_1} {β : Type u_2} [LinearOrder α] {b : α} {x : α} (f : (Set.Iic b)β) (hx : b x) :
              Set.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 : (Set.Icc a b)β) (hx : x a) :
              Set.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 : (Set.Icc a b)β) (hx : b x) :
              Set.IccExtend h f x = f b,
              @[simp]
              theorem Set.IciExtend_self {α : Type u_1} {β : Type u_2} [LinearOrder α] {a : α} (f : (Set.Ici a)β) :
              Set.IciExtend f a = f a,
              @[simp]
              theorem Set.IicExtend_self {α : Type u_1} {β : Type u_2} [LinearOrder α] {b : α} (f : (Set.Iic b)β) :
              Set.IicExtend f b = f b,
              @[simp]
              theorem Set.IccExtend_left {α : Type u_1} {β : Type u_2} [LinearOrder α] {a : α} {b : α} (h : a b) (f : (Set.Icc a b)β) :
              Set.IccExtend h f a = f a,
              @[simp]
              theorem Set.IccExtend_right {α : Type u_1} {β : Type u_2} [LinearOrder α] {a : α} {b : α} (h : a b) (f : (Set.Icc a b)β) :
              Set.IccExtend h f b = f b,
              theorem Set.IciExtend_of_mem {α : Type u_1} {β : Type u_2} [LinearOrder α] {a : α} {x : α} (f : (Set.Ici a)β) (hx : x Set.Ici a) :
              Set.IciExtend f x = f x, hx
              theorem Set.IicExtend_of_mem {α : Type u_1} {β : Type u_2} [LinearOrder α] {b : α} {x : α} (f : (Set.Iic b)β) (hx : x Set.Iic b) :
              Set.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 : (Set.Icc a b)β) (hx : x Set.Icc a b) :
              Set.IccExtend h f x = f x, hx
              @[simp]
              theorem Set.IciExtend_coe {α : Type u_1} {β : Type u_2} [LinearOrder α] {a : α} (f : (Set.Ici a)β) (x : (Set.Ici a)) :
              Set.IciExtend f x = f x
              @[simp]
              theorem Set.IicExtend_coe {α : Type u_1} {β : Type u_2} [LinearOrder α] {b : α} (f : (Set.Iic b)β) (x : (Set.Iic b)) :
              Set.IicExtend f x = f x
              @[simp]
              theorem Set.IccExtend_val {α : Type u_1} {β : Type u_2} [LinearOrder α] {a : α} {b : α} (h : a b) (f : (Set.Icc a b)β) (x : (Set.Icc a b)) :
              Set.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) :
              Set.IccExtend h (f Subtype.val) = f

              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 (Set.Ici a)} (hs : s.OrdConnected) :
              {x : α | Set.IciExtend (fun (x : (Set.Ici a)) => x s) x}.OrdConnected
              theorem Set.OrdConnected.IicExtend {α : Type u_1} [LinearOrder α] {b : α} {s : Set (Set.Iic b)} (hs : s.OrdConnected) :
              {x : α | Set.IicExtend (fun (x : (Set.Iic b)) => x s) x}.OrdConnected
              theorem Set.OrdConnected.restrict {α : Type u_1} [LinearOrder α] {s : Set α} {t : Set α} (hs : s.OrdConnected) :
              {x : t | t.restrict (fun (x : α) => x s) x}.OrdConnected