mathlib documentation

data.set.intervals.proj_Icc

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.proj_Icc {α : Type u_1} [linear_order α] (a b : α) (h : a b) (x : α) :

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

Equations
theorem set.proj_Icc_of_le_left {α : Type u_1} [linear_order α] {a b : α} (h : a b) {x : α} (hx : x a) :
set.proj_Icc a b h x = a, _⟩

@[simp]
theorem set.proj_Icc_left {α : Type u_1} [linear_order α] {a b : α} (h : a b) :
set.proj_Icc a 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) :
set.proj_Icc a b h x = b, _⟩

@[simp]
theorem set.proj_Icc_right {α : Type u_1} [linear_order α] {a b : α} (h : a b) :
set.proj_Icc a b h b = b, _⟩

theorem set.proj_Icc_of_mem {α : Type u_1} [linear_order α] {a b : α} (h : a b) {x : α} (hx : x set.Icc a b) :
set.proj_Icc a 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)) :
set.proj_Icc a 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_incr_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) :
set.Icc_extend h f 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) → β) :
set.Icc_extend h f 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) :
set.Icc_extend h f 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) → β) :
set.Icc_extend h f 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 set.Icc a b) :
set.Icc_extend h f 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)) :

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_incr_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) :