Projection of a line onto a closed interval #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Given a linearly ordered type α, in this file we define
set.proj_Ici (a : α)to be the mapα → [a, ∞[sending]-∞, a]toa, and each pointx ∈ [a, ∞[to itself;set.proj_Iic (b : α)to be the mapα → ]-∞, b[sending[b, ∞[tob, and each pointx ∈ ]-∞, b]to itself;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.Ici_extend {a : α} (f : Ici a → β)to be the extension offtoαdefined asf ∘ proj_Ici a.set.Iic_extend {b : α} (f : Iic b → β)to be the extension offtoαdefined asf ∘ proj_Iic b.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, ∞[.
Equations
- set.proj_Ici a x = ⟨linear_order.max a x, _⟩
Projection of α to the closed interval ]-∞, b].
Equations
- set.proj_Iic b x = ⟨linear_order.min b x, _⟩
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), _⟩
@[norm_cast]
theorem
set.coe_proj_Ici
{α : Type u_1}
[linear_order α]
(a x : α) :
↑(set.proj_Ici a x) = linear_order.max a x
@[norm_cast]
theorem
set.coe_proj_Iic
{α : Type u_1}
[linear_order α]
(b x : α) :
↑(set.proj_Iic b x) = linear_order.min b x
@[norm_cast]
theorem
set.coe_proj_Icc
{α : Type u_1}
[linear_order α]
(a b : α)
(h : a ≤ b)
(x : α) :
↑(set.proj_Icc a b h x) = linear_order.max a (linear_order.min b x)
theorem
set.proj_Ici_of_le
{α : Type u_1}
[linear_order α]
{a x : α}
(hx : x ≤ a) :
set.proj_Ici a x = ⟨a, _⟩
theorem
set.proj_Iic_of_le
{α : Type u_1}
[linear_order α]
{b x : α}
(hx : b ≤ x) :
set.proj_Iic b x = ⟨b, _⟩
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, _⟩
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]
@[simp]
@[simp]
theorem
set.proj_Icc_left
{α : Type u_1}
[linear_order α]
{a b : α}
(h : a ≤ b) :
set.proj_Icc a b h a = ⟨a, _⟩
@[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_Ici_eq_self
{α : Type u_1}
[linear_order α]
{a x : α} :
set.proj_Ici a x = ⟨a, _⟩ ↔ x ≤ a
theorem
set.proj_Iic_eq_self
{α : Type u_1}
[linear_order α]
{b x : α} :
set.proj_Iic b x = ⟨b, _⟩ ↔ b ≤ x
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_Ici_of_mem
{α : Type u_1}
[linear_order α]
{a x : α}
(hx : x ∈ set.Ici a) :
set.proj_Ici a x = ⟨x, hx⟩
theorem
set.proj_Iic_of_mem
{α : Type u_1}
[linear_order α]
{b x : α}
(hx : x ∈ set.Iic b) :
set.proj_Iic b x = ⟨x, hx⟩
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_Ici_coe
{α : Type u_1}
[linear_order α]
{a : α}
(x : ↥(set.Ici a)) :
set.proj_Ici a ↑x = x
@[simp]
theorem
set.proj_Iic_coe
{α : Type u_1}
[linear_order α]
{b : α}
(x : ↥(set.Iic b)) :
set.proj_Iic b ↑x = x
@[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_Ici_surj_on
{α : Type u_1}
[linear_order α]
{a : α} :
set.surj_on (set.proj_Ici a) (set.Ici a) set.univ
theorem
set.proj_Iic_surj_on
{α : Type u_1}
[linear_order α]
{b : α} :
set.surj_on (set.proj_Iic b) (set.Iic b) set.univ
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]
@[simp]
@[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_Ici
{α : Type u_1}
[linear_order α]
{a : α} :
strict_mono_on (set.proj_Ici a) (set.Ici a)
theorem
set.strict_mono_on_proj_Iic
{α : Type u_1}
[linear_order α]
{b : α} :
strict_mono_on (set.proj_Iic b) (set.Iic b)
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.Ici_extend
{α : Type u_1}
{β : Type u_2}
[linear_order α]
{a : α}
(f : ↥(set.Ici a) → β) :
α → β
Extend a function [a, ∞[ → β to a map α → β.
Equations
- set.Ici_extend f = f ∘ set.proj_Ici a
def
set.Iic_extend
{α : Type u_1}
{β : Type u_2}
[linear_order α]
{b : α}
(f : ↥(set.Iic b) → β) :
α → β
Extend a function ]-∞, b] → β to a map α → β.
Equations
- set.Iic_extend f = f ∘ set.proj_Iic 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.Ici_extend_apply
{α : Type u_1}
{β : Type u_2}
[linear_order α]
{a : α}
(f : ↥(set.Ici a) → β)
(x : α) :
set.Ici_extend f x = f ⟨linear_order.max a x, _⟩
@[simp]
theorem
set.Iic_extend_apply
{α : Type u_1}
{β : Type u_2}
[linear_order α]
{b : α}
(f : ↥(set.Iic b) → β)
(x : α) :
set.Iic_extend f x = f ⟨linear_order.min b x, _⟩
theorem
set.Icc_extend_apply
{α : Type u_1}
{β : Type u_2}
[linear_order α]
{a b : α}
(h : a ≤ b)
(f : ↥(set.Icc a b) → β)
(x : α) :
set.Icc_extend h f x = f ⟨linear_order.max a (linear_order.min b x), _⟩
@[simp]
theorem
set.range_Ici_extend
{α : Type u_1}
{β : Type u_2}
[linear_order α]
{a : α}
(f : ↥(set.Ici a) → β) :
set.range (set.Ici_extend f) = set.range f
@[simp]
theorem
set.range_Iic_extend
{α : Type u_1}
{β : Type u_2}
[linear_order α]
{b : α}
(f : ↥(set.Iic b) → β) :
set.range (set.Iic_extend f) = set.range f
@[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.Ici_extend_of_le
{α : Type u_1}
{β : Type u_2}
[linear_order α]
{a x : α}
(f : ↥(set.Ici a) → β)
(hx : x ≤ a) :
set.Ici_extend f x = f ⟨a, _⟩
theorem
set.Iic_extend_of_le
{α : Type u_1}
{β : Type u_2}
[linear_order α]
{b x : α}
(f : ↥(set.Iic b) → β)
(hx : b ≤ x) :
set.Iic_extend f x = f ⟨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, _⟩
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.Ici_extend_self
{α : Type u_1}
{β : Type u_2}
[linear_order α]
{a : α}
(f : ↥(set.Ici a) → β) :
set.Ici_extend f a = f ⟨a, _⟩
@[simp]
theorem
set.Iic_extend_self
{α : Type u_1}
{β : Type u_2}
[linear_order α]
{b : α}
(f : ↥(set.Iic b) → β) :
set.Iic_extend f b = f ⟨b, _⟩
@[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, _⟩
@[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.Ici_extend_of_mem
{α : Type u_1}
{β : Type u_2}
[linear_order α]
{a x : α}
(f : ↥(set.Ici a) → β)
(hx : x ∈ set.Ici a) :
set.Ici_extend f x = f ⟨x, hx⟩
theorem
set.Iic_extend_of_mem
{α : Type u_1}
{β : Type u_2}
[linear_order α]
{b x : α}
(f : ↥(set.Iic b) → β)
(hx : x ∈ set.Iic b) :
set.Iic_extend f x = f ⟨x, hx⟩
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.Ici_extend_coe
{α : Type u_1}
{β : Type u_2}
[linear_order α]
{a : α}
(f : ↥(set.Ici a) → β)
(x : ↥(set.Ici a)) :
set.Ici_extend f ↑x = f x
@[simp]
theorem
set.Iic_extend_coe
{α : Type u_1}
{β : Type u_2}
[linear_order α]
{b : α}
(f : ↥(set.Iic b) → β)
(x : ↥(set.Iic b)) :
set.Iic_extend f ↑x = f x
@[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
set.Icc_extend_eq_self
{α : Type u_1}
{β : Type u_2}
[linear_order α]
{a b : α}
(h : a ≤ b)
(f : α → β)
(ha : ∀ (x : α), x < a → f x = f a)
(hb : ∀ (x : α), b < x → f x = f b) :
set.Icc_extend h (f ∘ coe) = f
If f : α → β is a constant both on $(-∞, a]$ and on $[b, +∞)$, then the extension of this
function from $[a, b]$ to the whole line is equal to the original function.
@[protected]
theorem
monotone.Ici_extend
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[preorder β]
{a : α}
{f : ↥(set.Ici a) → β}
(hf : monotone f) :
@[protected]
theorem
monotone.Iic_extend
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[preorder β]
{b : α}
{f : ↥(set.Iic b) → β}
(hf : monotone f) :
@[protected]
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_Ici_extend
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[preorder β]
{a : α}
{f : ↥(set.Ici a) → β}
(hf : strict_mono f) :
strict_mono_on (set.Ici_extend f) (set.Ici a)
theorem
strict_mono.strict_mono_on_Iic_extend
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[preorder β]
{b : α}
{f : ↥(set.Iic b) → β}
(hf : strict_mono f) :
strict_mono_on (set.Iic_extend f) (set.Iic b)
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)
@[protected]
theorem
set.ord_connected.Ici_extend
{α : Type u_1}
[linear_order α]
{a : α}
{s : set ↥(set.Ici a)}
(hs : s.ord_connected) :
{x : α | set.Ici_extend (λ (_x : ↥(set.Ici a)), _x ∈ s) x}.ord_connected
@[protected]
theorem
set.ord_connected.Iic_extend
{α : Type u_1}
[linear_order α]
{b : α}
{s : set ↥(set.Iic b)}
(hs : s.ord_connected) :
{x : α | set.Iic_extend (λ (_x : ↥(set.Iic b)), _x ∈ s) x}.ord_connected
@[protected]
theorem
set.ord_connected.restrict
{α : Type u_1}
[linear_order α]
{s t : set α}
(hs : s.ord_connected) :
{x : ↥t | t.restrict (λ (_x : α), _x ∈ s) x}.ord_connected