# Projection of a line onto a closed interval #

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

• Set.projIci (a : α) to be the map α → [a, ∞) sending (-∞, a] to a, and each point x ∈ [a, ∞) to itself;
• Set.projIic (b : α) to be the map α → (-∞, b[ sending [b, ∞) to b, and each point x ∈ (-∞, b] to itself;
• Set.projIcc (a b : α) (h : a ≤ b) to be the map α → [a, b] sending (-∞, a] to a, [b, ∞) to b, and each point x ∈ [a, b] to itself;
• Set.IccExtend {a b : α} (h : a ≤ b) (f : Icc a b → β) to be the extension of f to α defined as f ∘ projIcc a b h.
• Set.IciExtend {a : α} (f : Ici a → β) to be the extension of f to α defined as f ∘ projIci a.
• Set.IicExtend {b : α} (f : Iic b → β) to be the extension of f to α defined as f ∘ projIic b.

We also prove some trivial properties of these maps.

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

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

Equations
• = max a x,
Instances For
def Set.projIic {α : Type u_1} [] (b : α) (x : α) :
()

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

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

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

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

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

Equations
Instances For
def Set.IccExtend {α : Type u_1} {β : Type u_2} [] {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} [] {a : α} (f : ()β) (x : α) :
= f max a x,
theorem Set.IicExtend_apply {α : Type u_1} {β : Type u_2} [] {b : α} (f : ()β) (x : α) :
= f min b x,
theorem Set.IccExtend_apply {α : Type u_1} {β : Type u_2} [] {a : α} {b : α} (h : a b) (f : (Set.Icc a b)β) (x : α) :
= f max a (min b x),
@[simp]
theorem Set.range_IciExtend {α : Type u_1} {β : Type u_2} [] {a : α} (f : ()β) :
@[simp]
theorem Set.range_IicExtend {α : Type u_1} {β : Type u_2} [] {b : α} (f : ()β) :
@[simp]
theorem Set.IccExtend_range {α : Type u_1} {β : Type u_2} [] {a : α} {b : α} (h : a b) (f : (Set.Icc a b)β) :
theorem Set.IciExtend_of_le {α : Type u_1} {β : Type u_2} [] {a : α} {x : α} (f : ()β) (hx : x a) :
= f a,
theorem Set.IicExtend_of_le {α : Type u_1} {β : Type u_2} [] {b : α} {x : α} (f : ()β) (hx : b x) :
= f b,
theorem Set.IccExtend_of_le_left {α : Type u_1} {β : Type u_2} [] {a : α} {b : α} (h : a b) {x : α} (f : (Set.Icc a b)β) (hx : x a) :
= f a,
theorem Set.IccExtend_of_right_le {α : Type u_1} {β : Type u_2} [] {a : α} {b : α} (h : a b) {x : α} (f : (Set.Icc a b)β) (hx : b x) :
= f b,
@[simp]
theorem Set.IciExtend_self {α : Type u_1} {β : Type u_2} [] {a : α} (f : ()β) :
= f a,
@[simp]
theorem Set.IicExtend_self {α : Type u_1} {β : Type u_2} [] {b : α} (f : ()β) :
= f b,
@[simp]
theorem Set.IccExtend_left {α : Type u_1} {β : Type u_2} [] {a : α} {b : α} (h : a b) (f : (Set.Icc a b)β) :
= f a,
@[simp]
theorem Set.IccExtend_right {α : Type u_1} {β : Type u_2} [] {a : α} {b : α} (h : a b) (f : (Set.Icc a b)β) :
= f b,
theorem Set.IciExtend_of_mem {α : Type u_1} {β : Type u_2} [] {a : α} {x : α} (f : ()β) (hx : x ) :
= f x, hx
theorem Set.IicExtend_of_mem {α : Type u_1} {β : Type u_2} [] {b : α} {x : α} (f : ()β) (hx : x ) :
= f x, hx
theorem Set.IccExtend_of_mem {α : Type u_1} {β : Type u_2} [] {a : α} {b : α} (h : a b) {x : α} (f : (Set.Icc a b)β) (hx : x Set.Icc a b) :
= f x, hx
@[simp]
theorem Set.IciExtend_coe {α : Type u_1} {β : Type u_2} [] {a : α} (f : ()β) (x : ()) :
= f x
@[simp]
theorem Set.IicExtend_coe {α : Type u_1} {β : Type u_2} [] {b : α} (f : ()β) (x : ()) :
= f x
@[simp]
theorem Set.IccExtend_val {α : Type u_1} {β : Type u_2} [] {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} [] {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} [] [] {a : α} {f : ()β} (hf : ) :
theorem Monotone.IicExtend {α : Type u_1} {β : Type u_2} [] [] {b : α} {f : ()β} (hf : ) :
theorem Monotone.IccExtend {α : Type u_1} {β : Type u_2} [] [] {a : α} {b : α} (h : a b) {f : (Set.Icc a b)β} (hf : ) :
theorem StrictMono.strictMonoOn_IciExtend {α : Type u_1} {β : Type u_2} [] [] {a : α} {f : ()β} (hf : ) :
theorem StrictMono.strictMonoOn_IicExtend {α : Type u_1} {β : Type u_2} [] [] {b : α} {f : ()β} (hf : ) :
theorem StrictMono.strictMonoOn_IccExtend {α : Type u_1} {β : Type u_2} [] [] {a : α} {b : α} (h : a b) {f : (Set.Icc a b)β} (hf : ) :
theorem Set.OrdConnected.IciExtend {α : Type u_1} [] {a : α} {s : Set ()} (hs : s.OrdConnected) :
{x : α | Set.IciExtend (fun (x : ()) => x s) x}.OrdConnected
theorem Set.OrdConnected.IicExtend {α : Type u_1} [] {b : α} {s : Set ()} (hs : s.OrdConnected) :
{x : α | Set.IicExtend (fun (x : ()) => x s) x}.OrdConnected
theorem Set.OrdConnected.restrict {α : Type u_1} [] {s : Set α} {t : Set α} (hs : s.OrdConnected) :
{x : t | t.restrict (fun (x : α) => x s) x}.OrdConnected