Projection of a line onto a closed interval #
Given a linearly ordered type α
, in this file we define
Set.projIcc (a b : α) (h : a ≤ b)
to be the mapα → [a, b]
sending(-∞, a]
toa
,[b, ∞)
tob
, and each pointx ∈ [a, b]
to itself;Set.IccExtend {a b : α} (h : a ≤ b) (f : Icc a b → β)
to be the extension off
toα
defined asf ∘ projIcc a b h
.
We also prove some trivial properties of these maps.
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)
:
theorem
Set.projIcc_eq_right
{α : Type u_1}
[inst : LinearOrder α]
{a : α}
{b : α}
{x : α}
(h : a < b)
:
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)
:
Function.Surjective (Set.projIcc a b h)
@[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)
:
Monotone (Set.projIcc a b h)
theorem
Set.strictMonoOn_projIcc
{α : Type u_1}
[inst : LinearOrder α]
{a : α}
{b : α}
(h : a ≤ b)
:
StrictMonoOn (Set.projIcc a b h) (Set.Icc 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
- Set.IccExtend h f = f ∘ Set.projIcc a b h
@[simp]
theorem
Set.IccExtend_range
{α : Type u_1}
{β : Type u_2}
[inst : LinearOrder α]
{a : α}
{b : α}
(h : a ≤ b)
(f : ↑(Set.Icc a b) → β)
:
Set.range (Set.IccExtend h f) = Set.range f
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)
:
Monotone (Set.IccExtend h 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)
:
StrictMonoOn (Set.IccExtend h f) (Set.Icc a b)