# mathlib3documentation

data.set.intervals.proj_Icc

# Projection of a line onto a closed interval #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

• set.proj_Ici (a : α) to be the map α → [a, ∞[ sending ]-∞, a] to a, and each point x ∈ [a, ∞[ to itself;
• set.proj_Iic (b : α) to be the map α → ]-∞, b[ sending [b, ∞[ to b, and each point x ∈ ]-∞, b] to itself;
• set.proj_Icc (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.Ici_extend {a : α} (f : Ici a → β) to be the extension of f to α defined as f ∘ proj_Ici a.
• set.Iic_extend {b : α} (f : Iic b → β) to be the extension of f to α defined as f ∘ proj_Iic b.
• set.Icc_extend {a b : α} (h : a ≤ b) (f : Icc a b → β) to be the extension of f to α defined as f ∘ proj_Icc a b h.

We also prove some trivial properties of these maps.

def set.proj_Ici {α : Type u_1} [linear_order α] (a x : α) :

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

Equations
def set.proj_Iic {α : Type u_1} [linear_order α] (b x : α) :

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

Equations
def set.proj_Icc {α : Type u_1} [linear_order α] (a b : α) (h : a b) (x : α) :

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

Equations
• b h x = x), _⟩
@[norm_cast]
theorem set.coe_proj_Ici {α : Type u_1} [linear_order α] (a x : α) :
x) =
@[norm_cast]
theorem set.coe_proj_Iic {α : Type u_1} [linear_order α] (b x : α) :
x) =
@[norm_cast]
theorem set.coe_proj_Icc {α : Type u_1} [linear_order α] (a b : α) (h : a b) (x : α) :
b h x) = x)
theorem set.proj_Ici_of_le {α : Type u_1} [linear_order α] {a x : α} (hx : x a) :
x = a, _⟩
theorem set.proj_Iic_of_le {α : Type u_1} [linear_order α] {b x : α} (hx : b x) :
x = b, _⟩
theorem set.proj_Icc_of_le_left {α : Type u_1} [linear_order α] {a b : α} (h : a b) {x : α} (hx : x a) :
b h x = a, _⟩
theorem set.proj_Icc_of_right_le {α : Type u_1} [linear_order α] {a b : α} (h : a b) {x : α} (hx : b x) :
b h x = b, _⟩
@[simp]
theorem set.proj_Ici_self {α : Type u_1} [linear_order α] (a : α) :
a = a, _⟩
@[simp]
theorem set.proj_Iic_self {α : Type u_1} [linear_order α] (b : α) :
b = b, _⟩
@[simp]
theorem set.proj_Icc_left {α : Type u_1} [linear_order α] {a b : α} (h : a b) :
b h a = a, _⟩
@[simp]
theorem set.proj_Icc_right {α : Type u_1} [linear_order α] {a b : α} (h : a b) :
b h b = b, _⟩
theorem set.proj_Ici_eq_self {α : Type u_1} [linear_order α] {a x : α} :
x = a, _⟩ x a
theorem set.proj_Iic_eq_self {α : Type u_1} [linear_order α] {b x : α} :
x = b, _⟩ b x
theorem set.proj_Icc_eq_left {α : Type u_1} [linear_order α] {a b x : α} (h : a < b) :
b _ x = a, _⟩ x a
theorem set.proj_Icc_eq_right {α : Type u_1} [linear_order α] {a b x : α} (h : a < b) :
b _ x = b, _⟩ b x
theorem set.proj_Ici_of_mem {α : Type u_1} [linear_order α] {a x : α} (hx : x ) :
x = x, hx⟩
theorem set.proj_Iic_of_mem {α : Type u_1} [linear_order α] {b x : α} (hx : x ) :
x = x, hx⟩
theorem set.proj_Icc_of_mem {α : Type u_1} [linear_order α] {a b : α} (h : a b) {x : α} (hx : x b) :
b h x = x, hx⟩
@[simp]
theorem set.proj_Ici_coe {α : Type u_1} [linear_order α] {a : α} (x : (set.Ici a)) :
= x
@[simp]
theorem set.proj_Iic_coe {α : Type u_1} [linear_order α] {b : α} (x : (set.Iic b)) :
= x
@[simp]
theorem set.proj_Icc_coe {α : Type u_1} [linear_order α] {a b : α} (h : a b) (x : (set.Icc a b)) :
b h x = x
theorem set.proj_Ici_surj_on {α : Type u_1} [linear_order α] {a : α} :
theorem set.proj_Iic_surj_on {α : Type u_1} [linear_order α] {b : α} :
theorem set.proj_Icc_surj_on {α : Type u_1} [linear_order α] {a b : α} (h : a b) :
theorem set.proj_Ici_surjective {α : Type u_1} [linear_order α] {a : α} :
theorem set.proj_Iic_surjective {α : Type u_1} [linear_order α] {b : α} :
theorem set.proj_Icc_surjective {α : Type u_1} [linear_order α] {a b : α} (h : a b) :
@[simp]
theorem set.range_proj_Ici {α : Type u_1} [linear_order α] {a : α} :
@[simp]
theorem set.range_proj_Iic {α : Type u_1} [linear_order α] {a : α} :
@[simp]
theorem set.range_proj_Icc {α : Type u_1} [linear_order α] {a b : α} (h : a b) :
theorem set.monotone_proj_Ici {α : Type u_1} [linear_order α] {a : α} :
theorem set.monotone_proj_Iic {α : Type u_1} [linear_order α] {a : α} :
theorem set.monotone_proj_Icc {α : Type u_1} [linear_order α] {a b : α} (h : a b) :
theorem set.strict_mono_on_proj_Ici {α : Type u_1} [linear_order α] {a : α} :
(set.Ici a)
theorem set.strict_mono_on_proj_Iic {α : Type u_1} [linear_order α] {b : α} :
(set.Iic b)
theorem set.strict_mono_on_proj_Icc {α : Type u_1} [linear_order α] {a b : α} (h : a b) :
def set.Ici_extend {α : Type u_1} {β : Type u_2} [linear_order α] {a : α} (f : (set.Ici a) β) :
α β

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

Equations
def set.Iic_extend {α : Type u_1} {β : Type u_2} [linear_order α] {b : α} (f : (set.Iic b) β) :
α β

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

Equations
def set.Icc_extend {α : Type u_1} {β : Type u_2} [linear_order α] {a b : α} (h : a b) (f : (set.Icc a b) β) :
α β

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

Equations
@[simp]
theorem set.Ici_extend_apply {α : Type u_1} {β : Type u_2} [linear_order α] {a : α} (f : (set.Ici a) β) (x : α) :
= f , _⟩
@[simp]
theorem set.Iic_extend_apply {α : Type u_1} {β : Type u_2} [linear_order α] {b : α} (f : (set.Iic b) β) (x : α) :
= f , _⟩
theorem set.Icc_extend_apply {α : Type u_1} {β : Type u_2} [linear_order α] {a b : α} (h : a b) (f : (set.Icc a b) β) (x : α) :
x = f x), _⟩
@[simp]
theorem set.range_Ici_extend {α : Type u_1} {β : Type u_2} [linear_order α] {a : α} (f : (set.Ici a) β) :
@[simp]
theorem set.range_Iic_extend {α : Type u_1} {β : Type u_2} [linear_order α] {b : α} (f : (set.Iic b) β) :
@[simp]
theorem set.Icc_extend_range {α : Type u_1} {β : Type u_2} [linear_order α] {a b : α} (h : a b) (f : (set.Icc a b) β) :
theorem set.Ici_extend_of_le {α : Type u_1} {β : Type u_2} [linear_order α] {a x : α} (f : (set.Ici a) β) (hx : x a) :
= f a, _⟩
theorem set.Iic_extend_of_le {α : Type u_1} {β : Type u_2} [linear_order α] {b x : α} (f : (set.Iic b) β) (hx : b x) :
= f b, _⟩
theorem set.Icc_extend_of_le_left {α : Type u_1} {β : Type u_2} [linear_order α] {a b : α} (h : a b) {x : α} (f : (set.Icc a b) β) (hx : x a) :
x = f a, _⟩
theorem set.Icc_extend_of_right_le {α : Type u_1} {β : Type u_2} [linear_order α] {a b : α} (h : a b) {x : α} (f : (set.Icc a b) β) (hx : b x) :
x = f b, _⟩
@[simp]
theorem set.Ici_extend_self {α : Type u_1} {β : Type u_2} [linear_order α] {a : α} (f : (set.Ici a) β) :
= f a, _⟩
@[simp]
theorem set.Iic_extend_self {α : Type u_1} {β : Type u_2} [linear_order α] {b : α} (f : (set.Iic b) β) :
= f b, _⟩
@[simp]
theorem set.Icc_extend_left {α : Type u_1} {β : Type u_2} [linear_order α] {a b : α} (h : a b) (f : (set.Icc a b) β) :
a = f a, _⟩
@[simp]
theorem set.Icc_extend_right {α : Type u_1} {β : Type u_2} [linear_order α] {a b : α} (h : a b) (f : (set.Icc a b) β) :
b = f b, _⟩
theorem set.Ici_extend_of_mem {α : Type u_1} {β : Type u_2} [linear_order α] {a x : α} (f : (set.Ici a) β) (hx : x ) :
= f x, hx⟩
theorem set.Iic_extend_of_mem {α : Type u_1} {β : Type u_2} [linear_order α] {b x : α} (f : (set.Iic b) β) (hx : x ) :
= f x, hx⟩
theorem set.Icc_extend_of_mem {α : Type u_1} {β : Type u_2} [linear_order α] {a b : α} (h : a b) {x : α} (f : (set.Icc a b) β) (hx : x b) :
x = f x, hx⟩
@[simp]
theorem set.Ici_extend_coe {α : Type u_1} {β : Type u_2} [linear_order α] {a : α} (f : (set.Ici a) β) (x : (set.Ici a)) :
= f x
@[simp]
theorem set.Iic_extend_coe {α : Type u_1} {β : Type u_2} [linear_order α] {b : α} (f : (set.Iic b) β) (x : (set.Iic b)) :
= f x
@[simp]
theorem set.Icc_extend_coe {α : Type u_1} {β : Type u_2} [linear_order α] {a b : α} (h : a b) (f : (set.Icc a b) β) (x : (set.Icc a b)) :
x = f x
theorem set.Icc_extend_eq_self {α : Type u_1} {β : Type u_2} [linear_order α] {a b : α} (h : a b) (f : α β) (ha : (x : α), x < a f x = f a) (hb : (x : α), b < x f x = f b) :
(f coe) = 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.

@[protected]
theorem monotone.Ici_extend {α : Type u_1} {β : Type u_2} [linear_order α] [preorder β] {a : α} {f : (set.Ici a) β} (hf : monotone f) :
@[protected]
theorem monotone.Iic_extend {α : Type u_1} {β : Type u_2} [linear_order α] [preorder β] {b : α} {f : (set.Iic b) β} (hf : monotone f) :
@[protected]
theorem monotone.Icc_extend {α : Type u_1} {β : Type u_2} [linear_order α] [preorder β] {a b : α} (h : a b) {f : (set.Icc a b) β} (hf : monotone f) :
theorem strict_mono.strict_mono_on_Ici_extend {α : Type u_1} {β : Type u_2} [linear_order α] [preorder β] {a : α} {f : (set.Ici a) β} (hf : strict_mono f) :
(set.Ici a)
theorem strict_mono.strict_mono_on_Iic_extend {α : Type u_1} {β : Type u_2} [linear_order α] [preorder β] {b : α} {f : (set.Iic b) β} (hf : strict_mono f) :
(set.Iic b)
theorem strict_mono.strict_mono_on_Icc_extend {α : Type u_1} {β : Type u_2} [linear_order α] [preorder β] {a b : α} (h : a b) {f : (set.Icc a b) β} (hf : strict_mono f) :
(set.Icc a b)
@[protected]
theorem set.ord_connected.Ici_extend {α : Type u_1} [linear_order α] {a : α} {s : set (set.Ici a)} (hs : s.ord_connected) :
{x : α | set.Ici_extend (λ (_x : (set.Ici a)), _x s) x}.ord_connected
@[protected]
theorem set.ord_connected.Iic_extend {α : Type u_1} [linear_order α] {b : α} {s : set (set.Iic b)} (hs : s.ord_connected) :
{x : α | set.Iic_extend (λ (_x : (set.Iic b)), _x s) x}.ord_connected
@[protected]
theorem set.ord_connected.restrict {α : Type u_1} [linear_order α] {s t : set α} (hs : s.ord_connected) :
{x : t | t.restrict (λ (_x : α), _x s) x}.ord_connected