Projection of a line onto a closed interval #

Given a linearly ordered type α, in this file we define

Set.projIci (a : α) to be the map α → [a, ∞) sending (-∞, a] to a, and each point x ∈ [a, ∞) to itself;
Set.projIic (b : α) to be the map α → (-∞, b[ sending [b, ∞) to b, and each point x ∈ (-∞, b] to itself;
Set.projIcc (a b : α) (h : a ≤ b) to be the map α → [a, b] sending (-∞, a] to a, [b, ∞) to b, and each point x ∈ [a, b] to itself;
Set.IccExtend {a b : α} (h : a ≤ b) (f : Icc a b → β) to be the extension of f to α defined as f ∘ projIcc a b h.
Set.IciExtend {a : α} (f : Ici a → β) to be the extension of f to α defined as f ∘ projIci a.
Set.IicExtend {b : α} (f : Iic b → β) to be the extension of f to α defined as f ∘ projIic b.

We also prove some trivial properties of these maps.

source

def Set.projIci {α : Type u_1} [LinearOrder α] (a : α) (x : α) :

↑(Set.Ici a)

Projection of α to the closed interval [a, ∞).

Equations

Set.projIci a x = ⟨max a x, ⋯⟩

Instances For

source

def Set.projIic {α : Type u_1} [LinearOrder α] (b : α) (x : α) :

↑(Set.Iic b)

Projection of α to the closed interval (-∞, b].

Equations

Set.projIic b x = ⟨min b x, ⋯⟩

Instances For

source

def Set.projIcc {α : Type u_1} [LinearOrder α] (a : α) (b : α) (h : a ≤ b) (x : α) :

↑(Set.Icc a b)

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

Equations

Set.projIcc a b h x = ⟨max a (min b x), ⋯⟩

Instances For

source

theorem Set.coe_projIci {α : Type u_1} [LinearOrder α] (a : α) (x : α) :

↑(Set.projIci a x) = max a x

source

theorem Set.coe_projIic {α : Type u_1} [LinearOrder α] (b : α) (x : α) :

↑(Set.projIic b x) = min b x

source

theorem Set.coe_projIcc {α : Type u_1} [LinearOrder α] (a : α) (b : α) (h : a ≤ b) (x : α) :

↑(Set.projIcc a b h x) = max a (min b x)

source

theorem Set.projIci_of_le {α : Type u_1} [LinearOrder α] {a : α} {x : α} (hx : x ≤ a) :

Set.projIci a x = ⟨a, ⋯⟩

source

theorem Set.projIic_of_le {α : Type u_1} [LinearOrder α] {b : α} {x : α} (hx : b ≤ x) :

Set.projIic b x = ⟨b, ⋯⟩

source

theorem Set.projIcc_of_le_left {α : Type u_1} [LinearOrder α] {a : α} {b : α} (h : a ≤ b) {x : α} (hx : x ≤ a) :

Set.projIcc a b h x = ⟨a, ⋯⟩

source

theorem Set.projIcc_of_right_le {α : Type u_1} [LinearOrder α] {a : α} {b : α} (h : a ≤ b) {x : α} (hx : b ≤ x) :

Set.projIcc a b h x = ⟨b, ⋯⟩

source

@[simp]

theorem Set.projIci_self {α : Type u_1} [LinearOrder α] (a : α) :

Set.projIci a a = ⟨a, ⋯⟩

source

@[simp]

theorem Set.projIic_self {α : Type u_1} [LinearOrder α] (b : α) :

Set.projIic b b = ⟨b, ⋯⟩

source

@[simp]

theorem Set.projIcc_left {α : Type u_1} [LinearOrder α] {a : α} {b : α} (h : a ≤ b) :

Set.projIcc a b h a = ⟨a, ⋯⟩

source

@[simp]

theorem Set.projIcc_right {α : Type u_1} [LinearOrder α] {a : α} {b : α} (h : a ≤ b) :

Set.projIcc a b h b = ⟨b, ⋯⟩

source

theorem Set.projIci_eq_self {α : Type u_1} [LinearOrder α] {a : α} {x : α} :

Set.projIci a x = ⟨a, ⋯⟩ ↔ x ≤ a

source

theorem Set.projIic_eq_self {α : Type u_1} [LinearOrder α] {b : α} {x : α} :

Set.projIic b x = ⟨b, ⋯⟩ ↔ b ≤ x

source

theorem Set.projIcc_eq_left {α : Type u_1} [LinearOrder α] {a : α} {b : α} {x : α} (h : a < b) :

Set.projIcc a b ⋯ x = ⟨a, ⋯⟩ ↔ x ≤ a

source

theorem Set.projIcc_eq_right {α : Type u_1} [LinearOrder α] {a : α} {b : α} {x : α} (h : a < b) :

Set.projIcc a b ⋯ x = ⟨b, ⋯⟩ ↔ b ≤ x

source

theorem Set.projIci_of_mem {α : Type u_1} [LinearOrder α] {a : α} {x : α} (hx : x ∈ Set.Ici a) :

Set.projIci a x = ⟨x, hx⟩

source

theorem Set.projIic_of_mem {α : Type u_1} [LinearOrder α] {b : α} {x : α} (hx : x ∈ Set.Iic b) :

Set.projIic b x = ⟨x, hx⟩

source

theorem Set.projIcc_of_mem {α : Type u_1} [LinearOrder α] {a : α} {b : α} (h : a ≤ b) {x : α} (hx : x ∈ Set.Icc a b) :

Set.projIcc a b h x = ⟨x, hx⟩

source

@[simp]

theorem Set.projIci_coe {α : Type u_1} [LinearOrder α] {a : α} (x : ↑(Set.Ici a)) :

Set.projIci a ↑x = x

source

@[simp]

theorem Set.projIic_coe {α : Type u_1} [LinearOrder α] {b : α} (x : ↑(Set.Iic b)) :

Set.projIic b ↑x = x

source

@[simp]

theorem Set.projIcc_val {α : Type u_1} [LinearOrder α] {a : α} {b : α} (h : a ≤ b) (x : ↑(Set.Icc a b)) :

Set.projIcc a b h ↑x = x

source

theorem Set.projIci_surjOn {α : Type u_1} [LinearOrder α] {a : α} :

Set.SurjOn (Set.projIci a) (Set.Ici a) Set.univ

source

theorem Set.projIic_surjOn {α : Type u_1} [LinearOrder α] {b : α} :

Set.SurjOn (Set.projIic b) (Set.Iic b) Set.univ

source

theorem Set.projIcc_surjOn {α : Type u_1} [LinearOrder α] {a : α} {b : α} (h : a ≤ b) :

Set.SurjOn (Set.projIcc a b h) (Set.Icc a b) Set.univ

source

theorem Set.projIci_surjective {α : Type u_1} [LinearOrder α] {a : α} :

Function.Surjective (Set.projIci a)

source

theorem Set.projIic_surjective {α : Type u_1} [LinearOrder α] {b : α} :

Function.Surjective (Set.projIic b)

source

theorem Set.projIcc_surjective {α : Type u_1} [LinearOrder α] {a : α} {b : α} (h : a ≤ b) :

Function.Surjective (Set.projIcc a b h)

source

@[simp]

theorem Set.range_projIci {α : Type u_1} [LinearOrder α] {a : α} :

Set.range (Set.projIci a) = Set.univ

source

@[simp]

theorem Set.range_projIic {α : Type u_1} [LinearOrder α] {a : α} :

Set.range (Set.projIic a) = Set.univ

source

@[simp]

theorem Set.range_projIcc {α : Type u_1} [LinearOrder α] {a : α} {b : α} (h : a ≤ b) :

Set.range (Set.projIcc a b h) = Set.univ

source

theorem Set.monotone_projIci {α : Type u_1} [LinearOrder α] {a : α} :

Monotone (Set.projIci a)

source

theorem Set.monotone_projIic {α : Type u_1} [LinearOrder α] {a : α} :

Monotone (Set.projIic a)

source

theorem Set.monotone_projIcc {α : Type u_1} [LinearOrder α] {a : α} {b : α} (h : a ≤ b) :

Monotone (Set.projIcc a b h)

source

theorem Set.strictMonoOn_projIci {α : Type u_1} [LinearOrder α] {a : α} :

StrictMonoOn (Set.projIci a) (Set.Ici a)

source

theorem Set.strictMonoOn_projIic {α : Type u_1} [LinearOrder α] {b : α} :

StrictMonoOn (Set.projIic b) (Set.Iic b)

source

theorem Set.strictMonoOn_projIcc {α : Type u_1} [LinearOrder α] {a : α} {b : α} (h : a ≤ b) :

StrictMonoOn (Set.projIcc a b h) (Set.Icc a b)

source

def Set.IciExtend {α : Type u_1} {β : Type u_2} [LinearOrder α] {a : α} (f : ↑(Set.Ici a) → β) :

α → β

Extend a function [a, ∞) → β to a map α → β.

Equations

Set.IciExtend f = f ∘ Set.projIci a

Instances For

source

def Set.IicExtend {α : Type u_1} {β : Type u_2} [LinearOrder α] {b : α} (f : ↑(Set.Iic b) → β) :

α → β

Extend a function (-∞, b] → β to a map α → β.

Equations

Set.IicExtend f = f ∘ Set.projIic b

Instances For

source

def Set.IccExtend {α : Type u_1} {β : Type u_2} [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

Instances For

source

theorem Set.IciExtend_apply {α : Type u_1} {β : Type u_2} [LinearOrder α] {a : α} (f : ↑(Set.Ici a) → β) (x : α) :

Set.IciExtend f x = f ⟨max a x, ⋯⟩

source

theorem Set.IicExtend_apply {α : Type u_1} {β : Type u_2} [LinearOrder α] {b : α} (f : ↑(Set.Iic b) → β) (x : α) :

Set.IicExtend f x = f ⟨min b x, ⋯⟩

source

theorem Set.IccExtend_apply {α : Type u_1} {β : Type u_2} [LinearOrder α] {a : α} {b : α} (h : a ≤ b) (f : ↑(Set.Icc a b) → β) (x : α) :

Set.IccExtend h f x = f ⟨max a (min b x), ⋯⟩

source

@[simp]

theorem Set.range_IciExtend {α : Type u_1} {β : Type u_2} [LinearOrder α] {a : α} (f : ↑(Set.Ici a) → β) :

Set.range (Set.IciExtend f) = Set.range f

source

@[simp]

theorem Set.range_IicExtend {α : Type u_1} {β : Type u_2} [LinearOrder α] {b : α} (f : ↑(Set.Iic b) → β) :

Set.range (Set.IicExtend f) = Set.range f

source

@[simp]

theorem Set.IccExtend_range {α : Type u_1} {β : Type u_2} [LinearOrder α] {a : α} {b : α} (h : a ≤ b) (f : ↑(Set.Icc a b) → β) :

Set.range (Set.IccExtend h f) = Set.range f

source

theorem Set.IciExtend_of_le {α : Type u_1} {β : Type u_2} [LinearOrder α] {a : α} {x : α} (f : ↑(Set.Ici a) → β) (hx : x ≤ a) :

Set.IciExtend f x = f ⟨a, ⋯⟩

source

theorem Set.IicExtend_of_le {α : Type u_1} {β : Type u_2} [LinearOrder α] {b : α} {x : α} (f : ↑(Set.Iic b) → β) (hx : b ≤ x) :

Set.IicExtend f x = f ⟨b, ⋯⟩

source

theorem Set.IccExtend_of_le_left {α : Type u_1} {β : Type u_2} [LinearOrder α] {a : α} {b : α} (h : a ≤ b) {x : α} (f : ↑(Set.Icc a b) → β) (hx : x ≤ a) :

Set.IccExtend h f x = f ⟨a, ⋯⟩

source

theorem Set.IccExtend_of_right_le {α : Type u_1} {β : Type u_2} [LinearOrder α] {a : α} {b : α} (h : a ≤ b) {x : α} (f : ↑(Set.Icc a b) → β) (hx : b ≤ x) :

Set.IccExtend h f x = f ⟨b, ⋯⟩

source

@[simp]

theorem Set.IciExtend_self {α : Type u_1} {β : Type u_2} [LinearOrder α] {a : α} (f : ↑(Set.Ici a) → β) :

Set.IciExtend f a = f ⟨a, ⋯⟩

source

@[simp]

theorem Set.IicExtend_self {α : Type u_1} {β : Type u_2} [LinearOrder α] {b : α} (f : ↑(Set.Iic b) → β) :

Set.IicExtend f b = f ⟨b, ⋯⟩

source

@[simp]

theorem Set.IccExtend_left {α : Type u_1} {β : Type u_2} [LinearOrder α] {a : α} {b : α} (h : a ≤ b) (f : ↑(Set.Icc a b) → β) :

Set.IccExtend h f a = f ⟨a, ⋯⟩

source

@[simp]

theorem Set.IccExtend_right {α : Type u_1} {β : Type u_2} [LinearOrder α] {a : α} {b : α} (h : a ≤ b) (f : ↑(Set.Icc a b) → β) :

Set.IccExtend h f b = f ⟨b, ⋯⟩

source

theorem Set.IciExtend_of_mem {α : Type u_1} {β : Type u_2} [LinearOrder α] {a : α} {x : α} (f : ↑(Set.Ici a) → β) (hx : x ∈ Set.Ici a) :

Set.IciExtend f x = f ⟨x, hx⟩

source

theorem Set.IicExtend_of_mem {α : Type u_1} {β : Type u_2} [LinearOrder α] {b : α} {x : α} (f : ↑(Set.Iic b) → β) (hx : x ∈ Set.Iic b) :

Set.IicExtend f x = f ⟨x, hx⟩

source

theorem Set.IccExtend_of_mem {α : Type u_1} {β : Type u_2} [LinearOrder α] {a : α} {b : α} (h : a ≤ b) {x : α} (f : ↑(Set.Icc a b) → β) (hx : x ∈ Set.Icc a b) :

Set.IccExtend h f x = f ⟨x, hx⟩

source

@[simp]

theorem Set.IciExtend_coe {α : Type u_1} {β : Type u_2} [LinearOrder α] {a : α} (f : ↑(Set.Ici a) → β) (x : ↑(Set.Ici a)) :

Set.IciExtend f ↑x = f x

source

@[simp]

theorem Set.IicExtend_coe {α : Type u_1} {β : Type u_2} [LinearOrder α] {b : α} (f : ↑(Set.Iic b) → β) (x : ↑(Set.Iic b)) :

Set.IicExtend f ↑x = f x

source

@[simp]

theorem Set.IccExtend_val {α : Type u_1} {β : Type u_2} [LinearOrder α] {a : α} {b : α} (h : a ≤ b) (f : ↑(Set.Icc a b) → β) (x : ↑(Set.Icc a b)) :

Set.IccExtend h f ↑x = f x

source

theorem Set.IccExtend_eq_self {α : Type u_1} {β : Type u_2} [LinearOrder α] {a : α} {b : α} (h : a ≤ b) (f : α → β) (ha : ∀ x < a, f x = f a) (hb : ∀ (x : α), b < x → f x = f b) :

Set.IccExtend h (f ∘ Subtype.val) = 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.

source

theorem Monotone.IciExtend {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {a : α} {f : ↑(Set.Ici a) → β} (hf : Monotone f) :

Monotone (Set.IciExtend f)

source

theorem Monotone.IicExtend {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {b : α} {f : ↑(Set.Iic b) → β} (hf : Monotone f) :

Monotone (Set.IicExtend f)

source

theorem Monotone.IccExtend {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {a : α} {b : α} (h : a ≤ b) {f : ↑(Set.Icc a b) → β} (hf : Monotone f) :

Monotone (Set.IccExtend h f)

source

theorem StrictMono.strictMonoOn_IciExtend {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {a : α} {f : ↑(Set.Ici a) → β} (hf : StrictMono f) :

StrictMonoOn (Set.IciExtend f) (Set.Ici a)

source

theorem StrictMono.strictMonoOn_IicExtend {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {b : α} {f : ↑(Set.Iic b) → β} (hf : StrictMono f) :

StrictMonoOn (Set.IicExtend f) (Set.Iic b)

source

theorem StrictMono.strictMonoOn_IccExtend {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {a : α} {b : α} (h : a ≤ b) {f : ↑(Set.Icc a b) → β} (hf : StrictMono f) :

StrictMonoOn (Set.IccExtend h f) (Set.Icc a b)

source

theorem Set.OrdConnected.IciExtend {α : Type u_1} [LinearOrder α] {a : α} {s : Set ↑(Set.Ici a)} (hs : s.OrdConnected) :

{x : α | Set.IciExtend (fun (x : ↑(Set.Ici a)) => x ∈ s) x}.OrdConnected

source

theorem Set.OrdConnected.IicExtend {α : Type u_1} [LinearOrder α] {b : α} {s : Set ↑(Set.Iic b)} (hs : s.OrdConnected) :

{x : α | Set.IicExtend (fun (x : ↑(Set.Iic b)) => x ∈ s) x}.OrdConnected

source

theorem Set.OrdConnected.restrict {α : Type u_1} [LinearOrder α] {s : Set α} {t : Set α} (hs : s.OrdConnected) :

{x : ↑t | t.restrict (fun (x : α) => x ∈ s) x}.OrdConnected

HepLean Documentation

Mathlib.Order.Interval.Set.ProjIcc

Projection of a line onto a closed interval #