mathlibdocumentation

data.set.intervals.proj_Icc

Projection of a line onto a closed interval #

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

• 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.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_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), _⟩
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, _⟩
@[simp]
theorem set.proj_Icc_left {α : Type u_1} [linear_order α] {a b : α} (h : a b) :
b h a = 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_Icc_right {α : Type u_1} [linear_order α] {a b : α} (h : a b) :
b h b = b, _⟩
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_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_Icc_coe {α : Type u_1} [linear_order α] {a b : α} (h : a b) (x : (set.Icc a b)) :
b h x = x
theorem set.proj_Icc_surj_on {α : Type u_1} [linear_order α] {a b : α} (h : a b) :
theorem set.proj_Icc_surjective {α : Type u_1} [linear_order α] {a b : α} (h : a b) :
@[simp]
theorem set.range_proj_Icc {α : Type u_1} [linear_order α] {a b : α} (h : a b) :
theorem set.monotone_proj_Icc {α : Type u_1} [linear_order α] {a b : α} (h : a b) :
theorem set.strict_mono_on_proj_Icc {α : Type u_1} [linear_order α] {a b : α} (h : a b) :
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.Icc_extend_range {α : Type u_1} {β : Type u_2} [linear_order α] {a b : α} (h : a b) (f : (set.Icc a 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, _⟩
@[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, _⟩
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.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.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.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 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_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)