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.projIcc {α : Type u_1} [inst : LinearOrder α] (a : α) (b : α) (h : a b) (x : α) :
↑(Set.Icc a b)

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

Equations
theorem Set.projIcc_of_le_left {α : Type u_1} [inst : LinearOrder α] {a : α} {b : α} (h : a b) {x : α} (hx : x a) :
Set.projIcc a b h x = { val := a, property := (_ : a Set.Icc a b) }
@[simp]
theorem Set.projIcc_left {α : Type u_1} [inst : LinearOrder α] {a : α} {b : α} (h : a b) :
Set.projIcc a b h a = { val := a, property := (_ : a Set.Icc a b) }
theorem Set.projIcc_of_right_le {α : Type u_1} [inst : 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.projIcc_right {α : Type u_1} [inst : LinearOrder α] {a : α} {b : α} (h : a b) :
Set.projIcc a b h b = { val := b, property := (_ : b Set.Icc a b) }
theorem Set.projIcc_eq_left {α : Type u_1} [inst : 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} [inst : 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.projIcc_of_mem {α : Type u_1} [inst : 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.projIcc_val {α : Type u_1} [inst : LinearOrder α] {a : α} {b : α} (h : a b) (x : ↑(Set.Icc a b)) :
Set.projIcc a b h x = x
theorem Set.projIcc_surjOn {α : Type u_1} [inst : 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} [inst : LinearOrder α] {a : α} {b : α} (h : a b) :
@[simp]
theorem Set.range_projIcc {α : Type u_1} [inst : LinearOrder α] {a : α} {b : α} (h : a b) :
Set.range (Set.projIcc a b h) = Set.univ
theorem Set.monotone_projIcc {α : Type u_1} [inst : LinearOrder α] {a : α} {b : α} (h : a b) :
theorem Set.strictMonoOn_projIcc {α : Type u_1} [inst : LinearOrder α] {a : α} {b : α} (h : a b) :
def Set.IccExtend {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] {a : α} {b : α} (h : a b) (f : ↑(Set.Icc a b)β) :
αβ

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

Equations
@[simp]
theorem Set.IccExtend_range {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] {a : α} {b : α} (h : a b) (f : ↑(Set.Icc a b)β) :
theorem Set.IccExtend_of_le_left {α : Type u_1} {β : Type u_2} [inst : 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) }
@[simp]
theorem Set.IccExtend_left {α : Type u_1} {β : Type u_2} [inst : 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) }
theorem Set.IccExtend_of_right_le {α : Type u_1} {β : Type u_2} [inst : 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.IccExtend_right {α : Type u_1} {β : Type u_2} [inst : 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.IccExtend_of_mem {α : Type u_1} {β : Type u_2} [inst : 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.Icc_extend_coe {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] {a : α} {b : α} (h : a b) (f : ↑(Set.Icc a b)β) (x : ↑(Set.Icc a b)) :
Set.IccExtend h f x = f x
theorem Monotone.IccExtend {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst : Preorder β] {a : α} {b : α} (h : a b) {f : ↑(Set.Icc a b)β} (hf : Monotone f) :
theorem StrictMono.strictMonoOn_IccExtend {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst : Preorder β] {a : α} {b : α} (h : a b) {f : ↑(Set.Icc a b)β} (hf : StrictMono f) :