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]toa,[b, ∞)tob, and each pointx ∈ [a, b]to itself;set.Icc_extend {a b : α} (h : a ≤ b) (f : Icc a b → β)to be the extension offtoαdefined asf ∘ proj_Icc a b h.
We also prove some trivial properties of these maps.
Projection of α to the closed interval [a, b].
Equations
- set.proj_Icc a b h x = ⟨linear_order.max a (linear_order.min b x), _⟩
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_eq_left
{α : Type u_1}
[linear_order α]
{a b x : α}
(h : a < b) :
set.proj_Icc a b _ x = ⟨a, _⟩ ↔ x ≤ a
theorem
set.proj_Icc_eq_right
{α : Type u_1}
[linear_order α]
{a b x : α}
(h : a < b) :
set.proj_Icc a b _ x = ⟨b, _⟩ ↔ b ≤ x
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) :
set.surj_on (set.proj_Icc a b h) (set.Icc a b) set.univ
theorem
set.proj_Icc_surjective
{α : Type u_1}
[linear_order α]
{a b : α}
(h : a ≤ b) :
function.surjective (set.proj_Icc a b h)
@[simp]
theorem
set.range_proj_Icc
{α : Type u_1}
[linear_order α]
{a b : α}
(h : a ≤ b) :
set.range (set.proj_Icc a b h) = set.univ
theorem
set.monotone_proj_Icc
{α : Type u_1}
[linear_order α]
{a b : α}
(h : a ≤ b) :
monotone (set.proj_Icc a b h)
theorem
set.strict_mono_on_proj_Icc
{α : Type u_1}
[linear_order α]
{a b : α}
(h : a ≤ b) :
strict_mono_on (set.proj_Icc a b h) (set.Icc 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
- set.Icc_extend h f = f ∘ set.proj_Icc a b h
@[simp]
theorem
set.Icc_extend_range
{α : Type u_1}
{β : Type u_2}
[linear_order α]
{a b : α}
(h : a ≤ b)
(f : ↥(set.Icc a b) → β) :
set.range (set.Icc_extend h f) = set.range f
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)) :
set.Icc_extend h f ↑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) :
monotone (set.Icc_extend h 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) :
strict_mono_on (set.Icc_extend h f) (set.Icc a b)