Documentation

Mathlib.Data.Set.Intervals.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 = { val := a, property := (_ : a a) }
        theorem Set.projIic_of_le {α : Type u_1} [LinearOrder α] {b : α} {x : α} (hx : b x) :
        Set.projIic b x = { val := b, property := (_ : b 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 = { val := a, property := (_ : a Set.Icc a b) }
        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 = { val := b, property := (_ : b Set.Icc a b) }
        @[simp]
        theorem Set.projIci_self {α : Type u_1} [LinearOrder α] (a : α) :
        Set.projIci a a = { val := a, property := (_ : a a) }
        @[simp]
        theorem Set.projIic_self {α : Type u_1} [LinearOrder α] (b : α) :
        Set.projIic b b = { val := b, property := (_ : b b) }
        @[simp]
        theorem Set.projIcc_left {α : Type u_1} [LinearOrder α] {a : α} {b : α} (h : a b) :
        Set.projIcc a b h a = { val := a, property := (_ : a Set.Icc a b) }
        @[simp]
        theorem Set.projIcc_right {α : Type u_1} [LinearOrder α] {a : α} {b : α} (h : a b) :
        Set.projIcc a b h b = { val := b, property := (_ : b Set.Icc a b) }
        theorem Set.projIci_eq_self {α : Type u_1} [LinearOrder α] {a : α} {x : α} :
        Set.projIci a x = { val := a, property := (_ : a a) } x a
        theorem Set.projIic_eq_self {α : Type u_1} [LinearOrder α] {b : α} {x : α} :
        Set.projIic b x = { val := b, property := (_ : b b) } b x
        theorem Set.projIcc_eq_left {α : Type u_1} [LinearOrder α] {a : α} {b : α} {x : α} (h : a < b) :
        Set.projIcc a b (_ : a b) x = { val := a, property := (_ : a Set.Icc a b) } x a
        theorem Set.projIcc_eq_right {α : Type u_1} [LinearOrder α] {a : α} {b : α} {x : α} (h : a < b) :
        Set.projIcc a b (_ : a b) x = { val := b, property := (_ : b Set.Icc a b) } b x
        theorem Set.projIci_of_mem {α : Type u_1} [LinearOrder α] {a : α} {x : α} (hx : x Set.Ici a) :
        Set.projIci a x = { val := x, property := hx }
        theorem Set.projIic_of_mem {α : Type u_1} [LinearOrder α] {b : α} {x : α} (hx : x Set.Iic b) :
        Set.projIic b x = { val := x, property := 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 = { val := x, property := 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 { val := max a x, property := (_ : a 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 { val := min b x, property := (_ : min b x b) }
              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 { val := max a (min b x), property := (_ : a max a (min b x) max a (min b x) b) }
              @[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 { val := a, property := (_ : a 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 { val := b, property := (_ : b 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 { val := a, property := (_ : a Set.Icc a b) }
              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 { val := b, property := (_ : b Set.Icc a b) }
              @[simp]
              theorem Set.IciExtend_self {α : Type u_1} {β : Type u_2} [LinearOrder α] {a : α} (f : ↑(Set.Ici a)β) :
              Set.IciExtend f a = f { val := a, property := (_ : a a) }
              @[simp]
              theorem Set.IicExtend_self {α : Type u_1} {β : Type u_2} [LinearOrder α] {b : α} (f : ↑(Set.Iic b)β) :
              Set.IicExtend f b = f { val := b, property := (_ : b 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 { val := a, property := (_ : a Set.Icc a b) }
              @[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 { val := b, property := (_ : b Set.Icc a 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 { val := x, property := 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 { val := x, property := 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 { val := x, property := 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 : α), x < af 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 : Set.OrdConnected s) :
              Set.OrdConnected {x | Set.IciExtend (fun x => x s) x}
              theorem Set.OrdConnected.IicExtend {α : Type u_1} [LinearOrder α] {b : α} {s : Set ↑(Set.Iic b)} (hs : Set.OrdConnected s) :
              Set.OrdConnected {x | Set.IicExtend (fun x => x s) x}
              theorem Set.OrdConnected.restrict {α : Type u_1} [LinearOrder α] {s : Set α} {t : Set α} (hs : Set.OrdConnected s) :
              Set.OrdConnected {x | Set.restrict t (fun x => x s) x}