Mathlib.Order.Interval.Set.ProjIcc

Set.projIci definition

(a x : α) : Ici a

Full source

/-- Projection of `α` to the closed interval `[a, ∞)`. -/
def projIci (a x : α) : Ici a := ⟨max a x, le_max_left _ _⟩

Projection onto the interval $[a, \infty)$

Informal description

The projection function maps any element $x$ in a linearly ordered type $\alpha$ to the closed interval $[a, \infty)$. Specifically, it sends $x$ to $a$ if $x \leq a$, and to $x$ itself if $x \geq a$. Formally, it is defined as $\max(a, x)$, ensuring the result lies in $[a, \infty)$.

Set.projIic definition

(b x : α) : Iic b

Full source

/-- Projection of `α` to the closed interval `(-∞, b]`. -/
def projIic (b x : α) : Iic b := ⟨min b x, min_le_left _ _⟩

Projection onto left-infinite right-closed interval $ (-\infty, b] $

Informal description

The function maps an element $ x $ in a linearly ordered type $ \alpha $ to the left-infinite right-closed interval $ (-\infty, b] $ by taking the minimum of $ b $ and $ x $. Specifically, it sends $ x $ to $ \min(b, x) $, ensuring the result lies within $ (-\infty, b] $.

Set.projIcc definition

(a b : α) (h : a ≤ b) (x : α) : Icc a b

Full source

/-- Projection of `α` to the closed interval `[a, b]`. -/
def projIcc (a b : α) (h : a ≤ b) (x : α) : Icc a b :=
  ⟨max a (min b x), le_max_left _ _, max_le h (min_le_left _ _)⟩

Projection onto a closed interval $[a, b]$

Informal description

The function $\text{projIcc}(a, b, h)$ maps any element $x$ in a linearly ordered type $\alpha$ to the closed interval $[a, b]$, where $h$ is a proof that $a \leq b$. Specifically, it sends $x$ to $\max(a, \min(b, x))$, ensuring the result lies within $[a, b]$.

Set.coe_projIci theorem

(a x : α) : (projIci a x : α) = max a x

Full source

@[norm_cast]
theorem coe_projIci (a x : α) : (projIci a x : α) = max a x := rfl

Projection onto $[a, \infty)$ equals maximum of $a$ and $x$

Informal description

For any elements $a$ and $x$ in a linearly ordered type $\alpha$, the projection of $x$ onto the interval $[a, \infty)$ is equal to the maximum of $a$ and $x$, i.e., $\text{projIci}(a, x) = \max(a, x)$.

Set.coe_projIic theorem

(b x : α) : (projIic b x : α) = min b x

Full source

@[norm_cast]
theorem coe_projIic (b x : α) : (projIic b x : α) = min b x := rfl

Projection Formula for $(-\infty, b]$: $\text{projIic}(b, x) = \min(b, x)$

Informal description

For any elements $b$ and $x$ in a linearly ordered type $\alpha$, the projection of $x$ onto the left-infinite right-closed interval $(-\infty, b]$ is equal to the minimum of $b$ and $x$, i.e., $\text{projIic}(b, x) = \min(b, x)$.

Set.coe_projIcc theorem

(a b : α) (h : a ≤ b) (x : α) : (projIcc a b h x : α) = max a (min b x)

Full source

@[norm_cast]
theorem coe_projIcc (a b : α) (h : a ≤ b) (x : α) : (projIcc a b h x : α) = max a (min b x) := rfl

Projection Formula for Closed Interval: $\text{projIcc}(a, b, h)(x) = \max(a, \min(b, x))$

Informal description

For any elements $a, b, x$ in a linearly ordered type $\alpha$ with $a \leq b$, the projection of $x$ onto the closed interval $[a, b]$ is given by $\max(a, \min(b, x))$.

Set.projIci_of_le theorem

(hx : x ≤ a) : projIci a x = ⟨a, le_rfl⟩

Full source

theorem projIci_of_le (hx : x ≤ a) : projIci a x = ⟨a, le_rfl⟩ := Subtype.ext <| max_eq_left hx

Projection onto $[a, \infty)$ for elements below $a$

Informal description

For any element $x$ in a linearly ordered type $\alpha$ and a fixed element $a \in \alpha$, if $x \leq a$, then the projection of $x$ onto the interval $[a, \infty)$ is equal to $a$.

Set.projIic_of_le theorem

(hx : b ≤ x) : projIic b x = ⟨b, le_rfl⟩

Full source

theorem projIic_of_le (hx : b ≤ x) : projIic b x = ⟨b, le_rfl⟩ := Subtype.ext <| min_eq_left hx

Projection onto $(-\infty, b]$ for elements above $b$

Informal description

For any elements $b$ and $x$ in a linearly ordered type $\alpha$, if $b \leq x$, then the projection of $x$ onto the left-infinite right-closed interval $(-\infty, b]$ is equal to $b$.

Set.projIcc_of_le_left theorem

(hx : x ≤ a) : projIcc a b h x = ⟨a, left_mem_Icc.2 h⟩

Full source

theorem projIcc_of_le_left (hx : x ≤ a) : projIcc a b h x = ⟨a, left_mem_Icc.2 h⟩ := by
  simp [projIcc, hx, hx.trans h]

Projection onto $[a, b]$ for elements below $a$

Informal description

For any elements $a, b, x$ in a linearly ordered type $\alpha$ with $a \leq b$, if $x \leq a$, then the projection of $x$ onto the closed interval $[a, b]$ is equal to $a$.

Set.projIcc_of_right_le theorem

(hx : b ≤ x) : projIcc a b h x = ⟨b, right_mem_Icc.2 h⟩

Full source

theorem projIcc_of_right_le (hx : b ≤ x) : projIcc a b h x = ⟨b, right_mem_Icc.2 h⟩ := by
  simp [projIcc, hx, h]

Projection onto $[a, b]$ for elements above $b$

Informal description

For any elements $a, b, x$ in a linearly ordered type $\alpha$ with $a \leq b$, if $b \leq x$, then the projection of $x$ onto the closed interval $[a, b]$ is equal to $b$.

Set.projIci_self theorem

(a : α) : projIci a a = ⟨a, le_rfl⟩

Full source

@[simp]
theorem projIci_self (a : α) : projIci a a = ⟨a, le_rfl⟩ := projIci_of_le le_rfl

Projection of $a$ onto $[a, \infty)$ at $a$ equals $a$

Informal description

For any element $a$ in a linearly ordered type $\alpha$, the projection of $a$ onto the interval $[a, \infty)$ is equal to $a$ itself, i.e., $\text{projIci}(a, a) = a$.

Set.projIic_self theorem

(b : α) : projIic b b = ⟨b, le_rfl⟩

Full source

@[simp]
theorem projIic_self (b : α) : projIic b b = ⟨b, le_rfl⟩ := projIic_of_le le_rfl

Projection of $b$ onto $(-\infty, b]$ at $b$ equals $b$

Informal description

For any element $b$ in a linearly ordered type $\alpha$, the projection of $b$ onto the left-infinite right-closed interval $(-\infty, b]$ is equal to $b$ itself, i.e., $\text{projIic}(b, b) = b$.

Set.projIcc_left theorem

: projIcc a b h a = ⟨a, left_mem_Icc.2 h⟩

Full source

@[simp]
theorem projIcc_left : projIcc a b h a = ⟨a, left_mem_Icc.2 h⟩ :=
  projIcc_of_le_left h le_rfl

Projection of Left Endpoint onto Closed Interval $[a, b]$

Informal description

For any elements $a$ and $b$ in a linearly ordered type $\alpha$ with $a \leq b$, the projection of $a$ onto the closed interval $[a, b]$ is equal to $a$.

Set.projIcc_right theorem

: projIcc a b h b = ⟨b, right_mem_Icc.2 h⟩

Full source

@[simp]
theorem projIcc_right : projIcc a b h b = ⟨b, right_mem_Icc.2 h⟩ :=
  projIcc_of_right_le h le_rfl

Projection of Right Endpoint onto Closed Interval

Informal description

For any elements $a$ and $b$ in a linearly ordered type $\alpha$ with $a \leq b$, the projection of $b$ onto the closed interval $[a, b]$ is equal to $b$.

Set.projIci_eq_self theorem

: projIci a x = ⟨a, le_rfl⟩ ↔ x ≤ a

Full source

theorem projIci_eq_self : projIciprojIci a x = ⟨a, le_rfl⟩ ↔ x ≤ a := by simp [projIci, Subtype.ext_iff]

Projection onto $[a, \infty)$ equals $\langle a, \text{le\_refl}\rangle$ iff $x \leq a$

Informal description

For any elements $a$ and $x$ in a linearly ordered type $\alpha$, the projection of $x$ onto the interval $[a, \infty)$ equals the pair $\langle a, \text{le\_refl}\rangle$ (where $\text{le\_refl}$ is a proof that $a \leq a$) if and only if $x \leq a$.

Set.projIic_eq_self theorem

: projIic b x = ⟨b, le_rfl⟩ ↔ b ≤ x

Full source

theorem projIic_eq_self : projIicprojIic b x = ⟨b, le_rfl⟩ ↔ b ≤ x := by simp [projIic, Subtype.ext_iff]

Projection onto $(-\infty, b]$ equals $\langle b, \text{le\_refl}\rangle$ iff $b \leq x$

Informal description

For any elements $b$ and $x$ in a linearly ordered type $\alpha$, the projection of $x$ onto the interval $(-\infty, b]$ equals the pair $\langle b, \text{le\_refl}\rangle$ (where $\text{le\_refl}$ is a proof that $b \leq b$) if and only if $b \leq x$.

Set.projIcc_eq_left theorem

(h : a < b) : projIcc a b h.le x = ⟨a, left_mem_Icc.mpr h.le⟩ ↔ x ≤ a

Full source

theorem projIcc_eq_left (h : a < b) : projIccprojIcc a b h.le x = ⟨a, left_mem_Icc.mpr h.le⟩ ↔ x ≤ a := by
  simp [projIcc, Subtype.ext_iff, h.not_le]

Projection onto Closed Interval Equals Left Endpoint iff $x \leq a$

Informal description

Let $\alpha$ be a linearly ordered type, and let $a, b \in \alpha$ with $a < b$. For any $x \in \alpha$, the projection of $x$ onto the closed interval $[a, b]$ equals the left endpoint $a$ (with proof that $a \in [a, b]$) if and only if $x \leq a$.

Set.projIcc_eq_right theorem

(h : a < b) : projIcc a b h.le x = ⟨b, right_mem_Icc.2 h.le⟩ ↔ b ≤ x

Full source

theorem projIcc_eq_right (h : a < b) : projIccprojIcc a b h.le x = ⟨b, right_mem_Icc.2 h.le⟩ ↔ b ≤ x := by
  simp [projIcc, Subtype.ext_iff, max_min_distrib_left, h.le, h.not_le]

Projection onto Closed Interval Equals Right Endpoint iff $b \leq x$

Informal description

Let $\alpha$ be a linearly ordered type, and let $a, b \in \alpha$ with $a < b$. For any $x \in \alpha$, the projection of $x$ onto the closed interval $[a, b]$ equals the right endpoint $b$ (with proof that $b \in [a, b]$) if and only if $b \leq x$.

Set.projIci_of_mem theorem

(hx : x ∈ Ici a) : projIci a x = ⟨x, hx⟩

Full source

theorem projIci_of_mem (hx : x ∈ Ici a) : projIci a x = ⟨x, hx⟩ := by simpa [projIci]

Projection onto $[a, \infty)$ Preserves Interior Points

Informal description

For any element $x$ in the interval $[a, \infty)$ of a linearly ordered type $\alpha$, the projection $\text{projIci}(a)$ maps $x$ to itself, i.e., $\text{projIci}(a)(x) = \langle x, hx \rangle$, where $hx$ is a proof that $x \in [a, \infty)$.

Set.projIic_of_mem theorem

(hx : x ∈ Iic b) : projIic b x = ⟨x, hx⟩

Full source

theorem projIic_of_mem (hx : x ∈ Iic b) : projIic b x = ⟨x, hx⟩ := by simpa [projIic]

Projection onto $(-\infty, b]$ Preserves Interior Points

Informal description

For any element $x$ in the left-infinite right-closed interval $(-\infty, b]$ of a linearly ordered type $\alpha$, the projection $\text{projIic}(b)$ maps $x$ to itself, i.e., $\text{projIic}(b)(x) = \langle x, hx \rangle$, where $hx$ is a proof that $x \in (-\infty, b]$.

Set.projIcc_of_mem theorem

(hx : x ∈ Icc a b) : projIcc a b h x = ⟨x, hx⟩

Full source

theorem projIcc_of_mem (hx : x ∈ Icc a b) : projIcc a b h x = ⟨x, hx⟩ := by
  simp [projIcc, hx.1, hx.2]

Projection onto Closed Interval Preserves Interior Points

Informal description

For any element $x$ in the closed interval $[a, b]$ of a linearly ordered type $\alpha$, the projection $\text{projIcc}(a, b, h)$ maps $x$ to itself, i.e., $\text{projIcc}(a, b, h)(x) = \langle x, hx \rangle$, where $hx$ is a proof that $x \in [a, b]$.

Set.projIci_coe theorem

(x : Ici a) : projIci a x = x

Full source

@[simp]
theorem projIci_coe (x : Ici a) : projIci a x = x := by cases x; apply projIci_of_mem

Projection onto $[a, \infty)$ is identity on interior points

Informal description

For any element $x$ in the closed interval $[a, \infty)$ of a linearly ordered type $\alpha$, the projection function $\text{projIci}(a)$ maps $x$ to itself, i.e., $\text{projIci}(a)(x) = x$.

Set.projIic_coe theorem

(x : Iic b) : projIic b x = x

Full source

@[simp]
theorem projIic_coe (x : Iic b) : projIic b x = x := by cases x; apply projIic_of_mem

Projection onto $(-\infty, b]$ is identity on interior points

Informal description

For any element $x$ in the left-infinite right-closed interval $(-\infty, b]$ of a linearly ordered type $\alpha$, the projection function $\text{projIic}(b)$ maps $x$ to itself, i.e., $\text{projIic}(b)(x) = x$.

Set.projIcc_val theorem

(x : Icc a b) : projIcc a b h x = x

Full source

@[simp]
theorem projIcc_val (x : Icc a b) : projIcc a b h x = x := by
  cases x
  apply projIcc_of_mem

Projection onto Closed Interval is Identity on Interior Points

Informal description

For any element $x$ in the closed interval $[a, b]$ of a linearly ordered type $\alpha$, the projection function $\text{projIcc}(a, b, h)$ maps $x$ to itself, i.e., $\text{projIcc}(a, b, h)(x) = x$.

Set.projIci_surjOn theorem

: SurjOn (projIci a) (Ici a) univ

Full source

theorem projIci_surjOn : SurjOn (projIci a) (Ici a) univ := fun x _ => ⟨x, x.2, projIci_coe x⟩

Surjectivity of Projection onto $[a, \infty)$

Informal description

The projection function $\text{projIci}(a)$ from a linearly ordered type $\alpha$ onto the closed interval $[a, \infty)$ is surjective, meaning that for every $y \in [a, \infty)$, there exists an $x \in \alpha$ such that $\text{projIci}(a)(x) = y$.

Set.projIic_surjOn theorem

: SurjOn (projIic b) (Iic b) univ

Full source

theorem projIic_surjOn : SurjOn (projIic b) (Iic b) univ := fun x _ => ⟨x, x.2, projIic_coe x⟩

Surjectivity of Projection onto $(-\infty, b]$

Informal description

The projection function $\text{projIic}_b : \alpha \to (-\infty, b]$ is surjective onto the interval $(-\infty, b]$. That is, for every $y \in (-\infty, b]$, there exists an $x \in \alpha$ such that $\text{projIic}_b(x) = y$.

Set.projIcc_surjOn theorem

: SurjOn (projIcc a b h) (Icc a b) univ

Full source

theorem projIcc_surjOn : SurjOn (projIcc a b h) (Icc a b) univ := fun x _ =>
  ⟨x, x.2, projIcc_val h x⟩

Surjectivity of Projection onto Closed Interval $[a, b]$

Informal description

The projection function $\text{projIcc}(a, b, h)$ maps the entire space $\alpha$ surjectively onto the closed interval $[a, b]$, where $h$ is a proof that $a \leq b$. In other words, for every $y \in [a, b]$, there exists an $x \in \alpha$ such that $\text{projIcc}(a, b, h)(x) = y$.

Set.projIci_surjective theorem

: Surjective (projIci a)

Full source

theorem projIci_surjective : Surjective (projIci a) := fun x => ⟨x, projIci_coe x⟩

Surjectivity of Projection onto $[a, \infty)$

Informal description

The projection function $\text{projIci}_a : \alpha \to [a, \infty)$ is surjective. That is, for every $y \in [a, \infty)$, there exists an $x \in \alpha$ such that $\text{projIci}_a(x) = y$.

Set.projIic_surjective theorem

: Surjective (projIic b)

Full source

theorem projIic_surjective : Surjective (projIic b) := fun x => ⟨x, projIic_coe x⟩

Surjectivity of Projection onto $(-\infty, b]$

Informal description

The projection function $\text{projIic}_b : \alpha \to (-\infty, b]$ is surjective. That is, for every $y \in (-\infty, b]$, there exists an $x \in \alpha$ such that $\text{projIic}_b(x) = y$.

Set.projIcc_surjective theorem

: Surjective (projIcc a b h)

Full source

theorem projIcc_surjective : Surjective (projIcc a b h) := fun x => ⟨x, projIcc_val h x⟩

Surjectivity of Projection onto Closed Interval $[a, b]$

Informal description

The projection function $\text{projIcc}_{a,b} : \alpha \to [a, b]$ is surjective. That is, for every $y \in [a, b]$, there exists an $x \in \alpha$ such that $\text{projIcc}_{a,b}(x) = y$.

Set.range_projIci theorem

: range (projIci a) = univ

Full source

@[simp]
theorem range_projIci : range (projIci a) = univ := projIci_surjective.range_eq

Range of Projection onto $[a, \infty)$ is Entire Codomain

Informal description

The range of the projection function $\text{projIci}_a : \alpha \to [a, \infty)$ is the entire codomain $[a, \infty)$. That is, for every $y \in [a, \infty)$, there exists an $x \in \alpha$ such that $\text{projIci}_a(x) = y$.

Set.range_projIic theorem

: range (projIic a) = univ

Full source

@[simp]
theorem range_projIic : range (projIic a) = univ := projIic_surjective.range_eq

Range of Projection onto $(-\infty, a]$ is Entire Interval

Informal description

The range of the projection function $\text{projIic}_a : \alpha \to (-\infty, a]$ is the entire codomain $(-\infty, a]$, i.e., $\text{range}(\text{projIic}_a) = (-\infty, a]$.

Set.range_projIcc theorem

: range (projIcc a b h) = univ

Full source

@[simp]
theorem range_projIcc : range (projIcc a b h) = univ :=
  (projIcc_surjective h).range_eq

Surjectivity of Projection onto Closed Interval $[a, b]$

Informal description

The range of the projection function $\text{projIcc}_{a,b} : \alpha \to [a, b]$ is the entire closed interval $[a, b]$, i.e., for every $y \in [a, b]$, there exists an $x \in \alpha$ such that $\text{projIcc}_{a,b}(x) = y$.

Set.monotone_projIci theorem

: Monotone (projIci a)

Full source

theorem monotone_projIci : Monotone (projIci a) := fun _ _ => max_le_max le_rfl

Monotonicity of Projection onto $[a, \infty)$

Informal description

For any element $a$ in a linearly ordered type $\alpha$, the projection function $\text{projIci}_a : \alpha \to [a, \infty)$ is monotone. That is, for any $x, y \in \alpha$ with $x \leq y$, we have $\text{projIci}_a(x) \leq \text{projIci}_a(y)$.

Set.monotone_projIic theorem

: Monotone (projIic a)

Full source

theorem monotone_projIic : Monotone (projIic a) := fun _ _ => min_le_min le_rfl

Monotonicity of Projection onto $(-\infty, a]$

Informal description

For any element $a$ in a linearly ordered type $\alpha$, the projection function $\text{projIic}_a : \alpha \to (-\infty, a]$ is monotone. That is, for any $x, y \in \alpha$ with $x \leq y$, we have $\text{projIic}_a(x) \leq \text{projIic}_a(y)$.

Set.monotone_projIcc theorem

: Monotone (projIcc a b h)

Full source

theorem monotone_projIcc : Monotone (projIcc a b h) := fun _ _ hxy =>
  max_le_max le_rfl <| min_le_min le_rfl hxy

Monotonicity of Projection onto Closed Interval $[a, b]$

Informal description

For any elements $a$ and $b$ in a linearly ordered type $\alpha$ with $a \leq b$, the projection function $\text{projIcc}_{a,b} : \alpha \to [a, b]$ is monotone. That is, for any $x, y \in \alpha$ with $x \leq y$, we have $\text{projIcc}_{a,b}(x) \leq \text{projIcc}_{a,b}(y)$.

Set.strictMonoOn_projIci theorem

: StrictMonoOn (projIci a) (Ici a)

Full source

theorem strictMonoOn_projIci : StrictMonoOn (projIci a) (Ici a) := fun x hx y hy hxy => by
  simpa only [projIci_of_mem, hx, hy]

Strict Monotonicity of Projection onto $[a, \infty)$ on Its Domain

Informal description

The projection function $\text{projIci}(a) : \alpha \to [a, \infty)$ is strictly monotone on the interval $[a, \infty)$. That is, for any $x, y \in [a, \infty)$ with $x < y$, we have $\text{projIci}(a)(x) < \text{projIci}(a)(y)$.

Set.strictMonoOn_projIic theorem

: StrictMonoOn (projIic b) (Iic b)

Full source

theorem strictMonoOn_projIic : StrictMonoOn (projIic b) (Iic b) := fun x hx y hy hxy => by
  simpa only [projIic_of_mem, hx, hy]

Strict Monotonicity of Projection onto $(-\infty, b]$ on Its Domain

Informal description

The projection function $\text{projIic}(b) : \alpha \to (-\infty, b]$, defined by $\text{projIic}(b)(x) = \min(b, x)$, is strictly monotone on the interval $(-\infty, b]$. That is, for any $x, y \in (-\infty, b]$ with $x < y$, we have $\text{projIic}(b)(x) < \text{projIic}(b)(y)$.

Set.strictMonoOn_projIcc theorem

: StrictMonoOn (projIcc a b h) (Icc a b)

Full source

theorem strictMonoOn_projIcc : StrictMonoOn (projIcc a b h) (Icc a b) := fun x hx y hy hxy => by
  simpa only [projIcc_of_mem, hx, hy]

Strict Monotonicity of Projection onto Closed Interval $[a, b]$ on Its Domain

Informal description

The projection function $\text{projIcc}(a, b, h) : \alpha \to [a, b]$ is strictly monotone on the closed interval $[a, b]$. That is, for any $x, y \in [a, b]$ with $x < y$, we have $\text{projIcc}(a, b, h)(x) < \text{projIcc}(a, b, h)(y)$.

Set.IciExtend definition

(f : Ici a → β) : α → β

Full source

/-- Extend a function `[a, ∞) → β` to a map `α → β`. -/
def IciExtend (f : Ici a → β) : α → β :=
  f ∘ projIci a

Extension of a function from $[a, \infty)$ to the entire type

Informal description

Given a function $ f : [a, \infty) \to \beta $, the extension $ \text{IciExtend}(f) : \alpha \to \beta $ is defined by composing $ f $ with the projection $ \text{projIci}(a) $, which maps any $ x \in \alpha $ to $ \max(a, x) \in [a, \infty) $.

Set.IicExtend definition

(f : Iic b → β) : α → β

Full source

/-- Extend a function `(-∞, b] → β` to a map `α → β`. -/
def IicExtend (f : Iic b → β) : α → β :=
  f ∘ projIic b

Extension of a function from $ (-\infty, b] $ to the entire type

Informal description

The function extends a given function $ f $ defined on the left-infinite right-closed interval $ (-\infty, b] $ to the entire type $ \alpha $ by composing $ f $ with the projection function $ \text{projIic}(b) $, which maps any $ x \in \alpha $ to $ \min(b, x) \in (-\infty, b] $.

Set.IccExtend definition

{a b : α} (h : a ≤ b) (f : Icc a b → β) : α → β

Full source

/-- Extend a function `[a, b] → β` to a map `α → β`. -/
def IccExtend {a b : α} (h : a ≤ b) (f : Icc a b → β) : α → β :=
  f ∘ projIcc a b h

Extension of a function from a closed interval to the entire type

Informal description

Given a function $ f $ defined on the closed interval $[a, b]$ in a linearly ordered type $\alpha$, the function $\text{IccExtend}(h, f)$ extends $ f $ to the entire type $\alpha$ by composing $ f $ with the projection $\text{projIcc}(a, b, h)$, which maps any $ x \in \alpha $ to $[a, b]$. Here, $ h $ is a proof that $ a \leq b $.

Set.IciExtend_apply theorem

(f : Ici a → β) (x : α) : IciExtend f x = f ⟨max a x, le_max_left _ _⟩

Full source

theorem IciExtend_apply (f : Ici a → β) (x : α) : IciExtend f x = f ⟨max a x, le_max_left _ _⟩ :=
  rfl

Evaluation of Extended Function on $[a, \infty)$

Informal description

For any function $f : [a, \infty) \to \beta$ and any element $x \in \alpha$, the extension $\text{IciExtend}(f)(x)$ equals $f(\max(a, x))$, where $\max(a, x)$ is considered as an element of $[a, \infty)$ via the proof that $a \leq \max(a, x)$.

Set.IicExtend_apply theorem

(f : Iic b → β) (x : α) : IicExtend f x = f ⟨min b x, min_le_left _ _⟩

Full source

theorem IicExtend_apply (f : Iic b → β) (x : α) : IicExtend f x = f ⟨min b x, min_le_left _ _⟩ :=
  rfl

Evaluation of Extended Function on $(-\infty, b]$

Informal description

For any function $f : (-\infty, b] \to \beta$ and any element $x \in \alpha$, the extension $\text{IicExtend}(f)(x)$ equals $f(\min(b, x))$, where $\min(b, x)$ is considered as an element of $(-\infty, b]$ via the proof that $\min(b, x) \leq b$.

Set.IccExtend_apply theorem

 (h : a ≤ b) (f : Icc a b → β) (x : α) :
  IccExtend h f x = f ⟨max a (min b x), le_max_left _ _, max_le h (min_le_left _ _)⟩

Full source

theorem IccExtend_apply (h : a ≤ b) (f : Icc a b → β) (x : α) :
    IccExtend h f x = f ⟨max a (min b x), le_max_left _ _, max_le h (min_le_left _ _)⟩ := rfl

Evaluation of Extended Function on Closed Interval: $\text{IccExtend}(h, f)(x) = f(\max(a, \min(b, x)))$

Informal description

Given a linearly ordered type $\alpha$, elements $a, b \in \alpha$ with $a \leq b$, a function $f : [a, b] \to \beta$, and any $x \in \alpha$, the extension $\text{IccExtend}(h, f)(x)$ equals $f(\max(a, \min(b, x)))$, where $\max(a, \min(b, x))$ is considered as an element of $[a, b]$ via the proofs that $a \leq \max(a, \min(b, x))$ and $\max(a, \min(b, x)) \leq b$.

Set.range_IciExtend theorem

(f : Ici a → β) : range (IciExtend f) = range f

Full source

@[simp]
theorem range_IciExtend (f : Ici a → β) : range (IciExtend f) = range f := by
  simp only [IciExtend, range_comp f, range_projIci, range_id', image_univ]

Range Preservation under Extension from $[a, \infty)$ to $\alpha$

Informal description

For any function $f : [a, \infty) \to \beta$, the range of its extension $\text{IciExtend}(f) : \alpha \to \beta$ equals the range of $f$. That is, $\text{range}(\text{IciExtend}(f)) = \text{range}(f)$.

Set.range_IicExtend theorem

(f : Iic b → β) : range (IicExtend f) = range f

Full source

@[simp]
theorem range_IicExtend (f : Iic b → β) : range (IicExtend f) = range f := by
  simp only [IicExtend, range_comp f, range_projIic, range_id', image_univ]

Range of Extended Function on $(-\infty, b]$ Equals Range of Original Function

Informal description

For any function $f : (-\infty, b] \to \beta$, the range of its extension $\text{IicExtend}(f) : \alpha \to \beta$ is equal to the range of $f$.

Set.IccExtend_range theorem

(f : Icc a b → β) : range (IccExtend h f) = range f

Full source

@[simp]
theorem IccExtend_range (f : Icc a b → β) : range (IccExtend h f) = range f := by
  simp only [IccExtend, range_comp f, range_projIcc, image_univ]

Range of Extended Function on $[a, b]$ Equals Range of Original Function

Informal description

For any function $ f : [a, b] \to \beta $ defined on the closed interval $[a, b]$ in a linearly ordered type $\alpha$, the range of its extension $\text{IccExtend}(h, f) : \alpha \to \beta$ is equal to the range of $ f $. That is, \[ \text{range}(\text{IccExtend}(h, f)) = \text{range}(f). \] Here, $ h $ is a proof that $ a \leq b $.

Set.IciExtend_of_le theorem

(f : Ici a → β) (hx : x ≤ a) : IciExtend f x = f ⟨a, le_rfl⟩

Full source

theorem IciExtend_of_le (f : Ici a → β) (hx : x ≤ a) : IciExtend f x = f ⟨a, le_rfl⟩ :=
  congr_arg f <| projIci_of_le hx

Extension of Function on $[a, \infty)$ for Elements Below $a$

Informal description

Let $f : [a, \infty) \to \beta$ be a function defined on the closed interval $[a, \infty)$ in a linearly ordered type $\alpha$. For any $x \in \alpha$ with $x \leq a$, the extension of $f$ to $\alpha$ via projection onto $[a, \infty)$ satisfies $\text{IciExtend}(f)(x) = f(a)$.

Set.IicExtend_of_le theorem

(f : Iic b → β) (hx : b ≤ x) : IicExtend f x = f ⟨b, le_rfl⟩

Full source

theorem IicExtend_of_le (f : Iic b → β) (hx : b ≤ x) : IicExtend f x = f ⟨b, le_rfl⟩ :=
  congr_arg f <| projIic_of_le hx

Extension of Function on $(-\infty, b]$ for Elements Above $b$

Informal description

Let $f : (-\infty, b] \to \beta$ be a function defined on the left-infinite right-closed interval $(-\infty, b]$ in a linearly ordered type $\alpha$. For any $x \in \alpha$ with $b \leq x$, the extension of $f$ to $\alpha$ via projection onto $(-\infty, b]$ satisfies $\text{IicExtend}(f)(x) = f(b)$.

Set.IccExtend_of_le_left theorem

(f : Icc a b → β) (hx : x ≤ a) : IccExtend h f x = f ⟨a, left_mem_Icc.2 h⟩

Full source

theorem IccExtend_of_le_left (f : Icc a b → β) (hx : x ≤ a) :
    IccExtend h f x = f ⟨a, left_mem_Icc.2 h⟩ :=
  congr_arg f <| projIcc_of_le_left h hx

Extension of Function on Closed Interval for Elements Below Left Endpoint

Informal description

Let $f : [a, b] \to \beta$ be a function defined on the closed interval $[a, b]$ in a linearly ordered type $\alpha$, where $a \leq b$. For any $x \in \alpha$ with $x \leq a$, the extension of $f$ to $\alpha$ via projection onto $[a, b]$ satisfies $\text{IccExtend}(h, f)(x) = f(a)$.

Set.IccExtend_of_right_le theorem

(f : Icc a b → β) (hx : b ≤ x) : IccExtend h f x = f ⟨b, right_mem_Icc.2 h⟩

Full source

theorem IccExtend_of_right_le (f : Icc a b → β) (hx : b ≤ x) :
    IccExtend h f x = f ⟨b, right_mem_Icc.2 h⟩ :=
  congr_arg f <| projIcc_of_right_le h hx

Extension of Function on Closed Interval for Elements Above Right Endpoint

Informal description

Let $f : [a, b] \to \beta$ be a function defined on the closed interval $[a, b]$ in a linearly ordered type $\alpha$, where $a \leq b$. For any $x \in \alpha$ with $x \geq b$, the extension of $f$ to $\alpha$ via projection onto $[a, b]$ satisfies $\text{IccExtend}(h, f)(x) = f(b)$.

Set.IciExtend_self theorem

(f : Ici a → β) : IciExtend f a = f ⟨a, le_rfl⟩

Full source

@[simp]
theorem IciExtend_self (f : Ici a → β) : IciExtend f a = f ⟨a, le_rfl⟩ :=
  IciExtend_of_le f le_rfl

Extension of Function on $[a, \infty)$ Evaluated at $a$ Equals $f(a)$

Informal description

For any function $f : [a, \infty) \to \beta$ defined on the left-closed right-infinite interval $[a, \infty)$, the extension $\text{IciExtend}(f)$ evaluated at $a$ satisfies $\text{IciExtend}(f)(a) = f(a)$.

Set.IicExtend_self theorem

(f : Iic b → β) : IicExtend f b = f ⟨b, le_rfl⟩

Full source

@[simp]
theorem IicExtend_self (f : Iic b → β) : IicExtend f b = f ⟨b, le_rfl⟩ :=
  IicExtend_of_le f le_rfl

Extension of Function on $(-\infty, b]$ Evaluated at $b$ Equals $f(b)$

Informal description

For any function $f : (-\infty, b] \to \beta$ defined on the left-infinite right-closed interval $(-\infty, b]$, the extension $\text{IicExtend}(f)$ evaluated at $b$ satisfies $\text{IicExtend}(f)(b) = f(b)$.

Set.IccExtend_left theorem

(f : Icc a b → β) : IccExtend h f a = f ⟨a, left_mem_Icc.2 h⟩

Full source

@[simp]
theorem IccExtend_left (f : Icc a b → β) : IccExtend h f a = f ⟨a, left_mem_Icc.2 h⟩ :=
  IccExtend_of_le_left h f le_rfl

Extension of Function on Closed Interval Evaluates to $f(a)$ at Left Endpoint

Informal description

For any function $f \colon [a, b] \to \beta$ defined on the closed interval $[a, b]$ in a linearly ordered type $\alpha$ (where $a \leq b$), the extension of $f$ to $\alpha$ via projection onto $[a, b]$ satisfies $\text{IccExtend}(h, f)(a) = f(a)$.

Set.IccExtend_right theorem

(f : Icc a b → β) : IccExtend h f b = f ⟨b, right_mem_Icc.2 h⟩

Full source

@[simp]
theorem IccExtend_right (f : Icc a b → β) : IccExtend h f b = f ⟨b, right_mem_Icc.2 h⟩ :=
  IccExtend_of_right_le h f le_rfl

Extension of Function on Closed Interval Evaluates to $f(b)$ at Right Endpoint

Informal description

For any function $f \colon [a, b] \to \beta$ defined on the closed interval $[a, b]$ in a linearly ordered type $\alpha$ (where $a \leq b$), the extension of $f$ to $\alpha$ via projection onto $[a, b]$ satisfies $\text{IccExtend}(h, f)(b) = f(b)$.

Set.IciExtend_of_mem theorem

(f : Ici a → β) (hx : x ∈ Ici a) : IciExtend f x = f ⟨x, hx⟩

Full source

theorem IciExtend_of_mem (f : Ici a → β) (hx : x ∈ Ici a) : IciExtend f x = f ⟨x, hx⟩ :=
  congr_arg f <| projIci_of_mem hx

Extension Preserves Values on $[a, \infty)$

Informal description

For any function $f : [a, \infty) \to \beta$ and any element $x \in [a, \infty)$, the extension of $f$ to the entire type $\alpha$ via projection satisfies $\text{IciExtend}(f)(x) = f(x)$.

Set.IicExtend_of_mem theorem

(f : Iic b → β) (hx : x ∈ Iic b) : IicExtend f x = f ⟨x, hx⟩

Full source

theorem IicExtend_of_mem (f : Iic b → β) (hx : x ∈ Iic b) : IicExtend f x = f ⟨x, hx⟩ :=
  congr_arg f <| projIic_of_mem hx

Extension of Function Preserves Values on $(-\infty, b]$

Informal description

For any function $f : (-\infty, b] \to \beta$ and any element $x \in (-\infty, b]$, the extension of $f$ to the entire type $\alpha$ via projection satisfies $\text{IicExtend}(f)(x) = f(x)$.

Set.IccExtend_of_mem theorem

(f : Icc a b → β) (hx : x ∈ Icc a b) : IccExtend h f x = f ⟨x, hx⟩

Full source

theorem IccExtend_of_mem (f : Icc a b → β) (hx : x ∈ Icc a b) : IccExtend h f x = f ⟨x, hx⟩ :=
  congr_arg f <| projIcc_of_mem h hx

Extension of Function Preserves Values on Closed Interval $[a, b]$

Informal description

For any function $ f : [a, b] \to \beta $ and any $ x \in [a, b] $, the extension $ \text{IccExtend}(h, f) $ of $ f $ to the entire type $ \alpha $ satisfies $ \text{IccExtend}(h, f)(x) = f(x) $, where $ h $ is a proof that $ a \leq b $.

Set.IciExtend_coe theorem

(f : Ici a → β) (x : Ici a) : IciExtend f x = f x

Full source

@[simp]
theorem IciExtend_coe (f : Ici a → β) (x : Ici a) : IciExtend f x = f x :=
  congr_arg f <| projIci_coe x

Extension of Function Preserves Values on $[a, \infty)$

Informal description

For any function $f \colon [a, \infty) \to \beta$ and any point $x \in [a, \infty)$, the extension $\text{IciExtend}(f)$ of $f$ to the entire type $\alpha$ satisfies $\text{IciExtend}(f)(x) = f(x)$.

Set.IicExtend_coe theorem

(f : Iic b → β) (x : Iic b) : IicExtend f x = f x

Full source

@[simp]
theorem IicExtend_coe (f : Iic b → β) (x : Iic b) : IicExtend f x = f x :=
  congr_arg f <| projIic_coe x

Extension of Function Preserves Values on $(-\infty, b]$

Informal description

For any function $f \colon (-\infty, b] \to \beta$ and any point $x$ in the interval $(-\infty, b]$, the extension $\text{IicExtend}(f)$ of $f$ to the entire type $\alpha$ satisfies $\text{IicExtend}(f)(x) = f(x)$.

Set.IccExtend_val theorem

(f : Icc a b → β) (x : Icc a b) : IccExtend h f x = f x

Full source

@[simp]
theorem IccExtend_val (f : Icc a b → β) (x : Icc a b) : IccExtend h f x = f x :=
  congr_arg f <| projIcc_val h x

Extension of Function Preserves Values on Closed Interval $[a, b]$

Informal description

For any function $f \colon [a, b] \to \beta$ and any point $x \in [a, b]$, the extension $\text{IccExtend}(h, f)$ of $f$ to the entire type $\alpha$ satisfies $\text{IccExtend}(h, f)(x) = f(x)$.

Set.IccExtend_eq_self theorem

(f : α → β) (ha : ∀ x < a, f x = f a) (hb : ∀ x, b < x → f x = f b) : IccExtend h (f ∘ (↑)) = f

Full source

/-- 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. -/
theorem IccExtend_eq_self (f : α → β) (ha : ∀ x < a, f x = f a) (hb : ∀ x, b < x → f x = f b) :
    IccExtend h (f ∘ (↑)) = f := by
  ext x
  rcases lt_or_le x a with hxa | hax
  · simp [IccExtend_of_le_left _ _ hxa.le, ha x hxa]
  · rcases le_or_lt x b with hxb | hbx
    · lift x to Icc a b using ⟨hax, hxb⟩
      rw [IccExtend_val, comp_apply]
    · simp [IccExtend_of_right_le _ _ hbx.le, hb x hbx]

Extension of Constant-Ended Function Equals Original Function

Informal description

Let $f \colon \alpha \to \beta$ be a function that is constant on $(-\infty, a]$ and on $[b, +\infty)$. Then the extension of $f$ restricted to the closed interval $[a, b]$ via projection is equal to $f$ itself, i.e., $\text{IccExtend}(h, f \circ \iota) = f$, where $\iota \colon [a, b] \hookrightarrow \alpha$ is the inclusion map and $h$ is a proof that $a \leq b$.

Monotone.IciExtend theorem

{f : Ici a → β} (hf : Monotone f) : Monotone (IciExtend f)

Full source

protected theorem Monotone.IciExtend {f : Ici a → β} (hf : Monotone f) : Monotone (IciExtend f) :=
  hf.comp monotone_projIci

Monotonicity of the Extension from $[a, \infty)$ to $\alpha$

Informal description

Let $\alpha$ be a linearly ordered type and $\beta$ be any type. Given a monotone function $f : [a, \infty) \to \beta$, its extension $\text{IciExtend}(f) : \alpha \to \beta$ (defined by $\text{IciExtend}(f)(x) = f(\max(a, x))$) is also monotone.

Monotone.IicExtend theorem

{f : Iic b → β} (hf : Monotone f) : Monotone (IicExtend f)

Full source

protected theorem Monotone.IicExtend {f : Iic b → β} (hf : Monotone f) : Monotone (IicExtend f) :=
  hf.comp monotone_projIic

Monotonicity of the Extension from $(-\infty, b]$ to $\alpha$

Informal description

Let $\alpha$ be a linearly ordered type and $\beta$ be any type. Given a monotone function $f : (-\infty, b] \to \beta$, its extension $\text{IicExtend}(f) : \alpha \to \beta$ (defined by $\text{IicExtend}(f)(x) = f(\min(b, x))$) is also monotone.

Monotone.IccExtend theorem

(hf : Monotone f) : Monotone (IccExtend h f)

Full source

protected theorem Monotone.IccExtend (hf : Monotone f) : Monotone (IccExtend h f) :=
  hf.comp <| monotone_projIcc h

Monotonicity of the Extension from $[a, b]$ to $\alpha$

Informal description

Let $\alpha$ be a linearly ordered type, $a, b \in \alpha$ with $a \leq b$, and $\beta$ be any type. Given a monotone function $f : [a, b] \to \beta$, the extended function $\text{IccExtend}(h, f) : \alpha \to \beta$ (defined by $\text{IccExtend}(h, f)(x) = f(\text{projIcc}(a, b, h)(x))$) is also monotone. Here, $\text{projIcc}(a, b, h)$ projects any $x \in \alpha$ to $[a, b]$ by taking $\max(a, \min(b, x))$.

StrictMono.strictMonoOn_IciExtend theorem

{f : Ici a → β} (hf : StrictMono f) : StrictMonoOn (IciExtend f) (Ici a)

Full source

theorem StrictMono.strictMonoOn_IciExtend {f : Ici a → β} (hf : StrictMono f) :
    StrictMonoOn (IciExtend f) (Ici a) :=
  hf.comp_strictMonoOn strictMonoOn_projIci

Strict Monotonicity of the Extension from $[a, \infty)$ to $\alpha$ on $[a, \infty)$

Informal description

Let $\alpha$ be a linearly ordered type and $\beta$ be any type. Given a strictly monotone function $f : [a, \infty) \to \beta$, its extension $\text{IciExtend}(f) : \alpha \to \beta$ (defined by $\text{IciExtend}(f)(x) = f(\max(a, x))$) is strictly monotone on the interval $[a, \infty)$. That is, for any $x, y \in [a, \infty)$ with $x < y$, we have $\text{IciExtend}(f)(x) < \text{IciExtend}(f)(y)$.

StrictMono.strictMonoOn_IicExtend theorem

{f : Iic b → β} (hf : StrictMono f) : StrictMonoOn (IicExtend f) (Iic b)

Full source

theorem StrictMono.strictMonoOn_IicExtend {f : Iic b → β} (hf : StrictMono f) :
    StrictMonoOn (IicExtend f) (Iic b) :=
  hf.comp_strictMonoOn strictMonoOn_projIic

Strict Monotonicity of Extended Function on $(-\infty, b]$

Informal description

Let $\alpha$ be a linearly ordered type and $\beta$ any type. Given a strictly monotone function $f : (-\infty, b] \to \beta$, its extension $\text{IicExtend}(f) : \alpha \to \beta$ (defined by $\text{IicExtend}(f)(x) = f(\min(b, x))$) is strictly monotone on the interval $(-\infty, b]$. That is, for any $x, y \in (-\infty, b]$ with $x < y$, we have $\text{IicExtend}(f)(x) < \text{IicExtend}(f)(y)$.

StrictMono.strictMonoOn_IccExtend theorem

(hf : StrictMono f) : StrictMonoOn (IccExtend h f) (Icc a b)

Full source

theorem StrictMono.strictMonoOn_IccExtend (hf : StrictMono f) :
    StrictMonoOn (IccExtend h f) (Icc a b) :=
  hf.comp_strictMonoOn (strictMonoOn_projIcc h)

Strict Monotonicity of Extended Function on Closed Interval $[a, b]$

Informal description

Let $\alpha$ be a linearly ordered type and $\beta$ any type. Given a strictly monotone function $f : [a, b] \to \beta$ and a proof $h$ that $a \leq b$, the extended function $\text{IccExtend}(h, f) : \alpha \to \beta$ (defined by $\text{IccExtend}(h, f)(x) = f(\text{projIcc}(a, b, h)(x))$) is strictly monotone on the interval $[a, b]$. That is, for any $x, y \in [a, b]$ with $x < y$, we have $\text{IccExtend}(h, f)(x) < \text{IccExtend}(h, f)(y)$.

Set.OrdConnected.IciExtend theorem

{s : Set (Ici a)} (hs : s.OrdConnected) : {x | IciExtend (· ∈ s) x}.OrdConnected

Full source

protected theorem Set.OrdConnected.IciExtend {s : Set (Ici a)} (hs : s.OrdConnected) :
    {x | IciExtend (· ∈ s) x}.OrdConnected :=
  ⟨fun _ hx _ hy _ hz => hs.out hx hy ⟨max_le_max le_rfl hz.1, max_le_max le_rfl hz.2⟩⟩

Order-Connectedness of Extended Set via Ici Projection

Informal description

Let $\alpha$ be a linearly ordered type and $a \in \alpha$. For any order-connected subset $s$ of the interval $[a, \infty)$, the set $\{x \in \alpha \mid \text{IciExtend}(\cdot \in s)(x)\}$ is order-connected, where $\text{IciExtend}$ extends the indicator function of $s$ to all of $\alpha$ via composition with the projection $\text{projIci}(a)$.

Set.OrdConnected.IicExtend theorem

{s : Set (Iic b)} (hs : s.OrdConnected) : {x | IicExtend (· ∈ s) x}.OrdConnected

Full source

protected theorem Set.OrdConnected.IicExtend {s : Set (Iic b)} (hs : s.OrdConnected) :
    {x | IicExtend (· ∈ s) x}.OrdConnected :=
  ⟨fun _ hx _ hy _ hz => hs.out hx hy ⟨min_le_min le_rfl hz.1, min_le_min le_rfl hz.2⟩⟩

Order-Connectedness of Extended Set via Iic Projection

Informal description

Let $s$ be an order-connected subset of the left-infinite right-closed interval $(-\infty, b]$ in a linearly ordered type $\alpha$. Then the set $\{x \in \alpha \mid \text{IicExtend}(\cdot \in s)(x)\}$ is order-connected, where $\text{IicExtend}$ extends the indicator function of $s$ to all of $\alpha$ via composition with the projection $\text{projIic}(b)$.

Set.OrdConnected.restrict theorem

(hs : s.OrdConnected) : {x | restrict t (· ∈ s) x}.OrdConnected

Full source

protected theorem Set.OrdConnected.restrict (hs : s.OrdConnected) :
    {x | restrict t (· ∈ s) x}.OrdConnected :=
  ⟨fun _ hx _ hy _ hz => hs.out hx hy hz⟩

Order-Connectedness is Preserved Under Restriction

Informal description

Let $s$ be an order-connected subset of a linearly ordered type $\alpha$. Then for any subset $t \subseteq \alpha$, the set $\{x \in t \mid x \in s\}$ is also order-connected.