Mathlib.Order.Interval.Finset.Fin

Fin.instLocallyFiniteOrder instance

(n : ℕ) : LocallyFiniteOrder (Fin n)

Full source

instance instLocallyFiniteOrder (n : ℕ) : LocallyFiniteOrder (Fin n) where
  finsetIcc a b := attachFin (Icc a b) fun x hx ↦ (mem_Icc.mp hx).2.trans_lt b.2
  finsetIco a b := attachFin (Ico a b) fun x hx ↦ (mem_Ico.mp hx).2.trans b.2
  finsetIoc a b := attachFin (Ioc a b) fun x hx ↦ (mem_Ioc.mp hx).2.trans_lt b.2
  finsetIoo a b := attachFin (Ioo a b) fun x hx ↦ (mem_Ioo.mp hx).2.trans b.2
  finset_mem_Icc a b := by simp
  finset_mem_Ico a b := by simp
  finset_mem_Ioc a b := by simp
  finset_mem_Ioo a b := by simp

Locally Finite Order Structure on Finite Types $\text{Fin}(n)$

Informal description

For any natural number $n$, the type $\text{Fin}(n)$ of natural numbers less than $n$ is equipped with a locally finite order structure. This means that for any two elements $a, b \in \text{Fin}(n)$, the intervals $[a, b]$, $[a, b)$, $(a, b]$, and $(a, b)$ are all finite sets.

Fin.instLocallyFiniteOrderBot instance

: ∀ n, LocallyFiniteOrderBot (Fin n)

Full source

instance instLocallyFiniteOrderBot : ∀ n, LocallyFiniteOrderBot (Fin n)
  | 0 => IsEmpty.toLocallyFiniteOrderBot
  | _ + 1 => inferInstance

Locally Finite Order with Finite Lower-Bounded Intervals on $\text{Fin}(n)$

Informal description

For any natural number $n$, the type $\text{Fin}(n)$ of natural numbers less than $n$ is equipped with a locally finite order structure where all intervals bounded below are finite. This means that for any element $a \in \text{Fin}(n)$, the intervals $\operatorname{Iic}(a) = [\bot, a]$ and $\operatorname{Iio}(a) = (\bot, a)$ can be represented as finite sets.

Fin.instLocallyFiniteOrderTop instance

: ∀ n, LocallyFiniteOrderTop (Fin n)

Full source

instance instLocallyFiniteOrderTop : ∀ n, LocallyFiniteOrderTop (Fin n)
  | 0 => IsEmpty.toLocallyFiniteOrderTop
  | _ + 1 => inferInstance

Locally Finite Order with Finite Upper-Bounded Intervals on $\text{Fin}(n)$

Informal description

For any natural number $n$, the type $\text{Fin}(n)$ of natural numbers less than $n$ is equipped with a locally finite order structure where all intervals bounded above are finite. This means that for any element $a \in \text{Fin}(n)$, the intervals $\operatorname{Ici}(a) = [a, \top]$ and $\operatorname{Ioi}(a) = (a, \top]$ can be represented as finite sets.

Fin.attachFin_Icc theorem

: attachFin (Icc a b) (fun _x hx ↦ (mem_Icc.mp hx).2.trans_lt b.2) = Icc a b

Full source

@[simp]
theorem attachFin_Icc :
    attachFin (Icc a b) (fun _x hx ↦ (mem_Icc.mp hx).2.trans_lt b.2) = Icc a b :=
  rfl

$\text{attachFin}$ Preserves Closed Interval in $\text{Fin}(n)$

Informal description

For any elements $a, b$ in $\text{Fin}(n)$, the operation $\text{attachFin}$ applied to the closed interval $\text{Icc}(a, b)$ (with a proof that all elements in the interval are less than $b$) yields the same interval $\text{Icc}(a, b)$. Here, $\text{attachFin}$ is a function that attaches a proof to each element in the interval that it is indeed a valid element of $\text{Fin}(n)$, and $\text{Icc}(a, b)$ denotes the set $\{x \in \text{Fin}(n) \mid a \leq x \leq b\}$.

Fin.attachFin_Ico theorem

: attachFin (Ico a b) (fun _x hx ↦ (mem_Ico.mp hx).2.trans b.2) = Ico a b

Full source

@[simp]
theorem attachFin_Ico :
    attachFin (Ico a b) (fun _x hx ↦ (mem_Ico.mp hx).2.trans b.2) = Ico a b :=
  rfl

$\text{attachFin}$ Preserves Closed-Open Interval in $\text{Fin}(n)$

Informal description

For any elements $a, b$ in $\text{Fin}(n)$, the operation $\text{attachFin}$ applied to the closed-open interval $\text{Ico}(a, b)$ (with a proof that all elements in the interval are less than $b$) yields the same interval $\text{Ico}(a, b)$. Here, $\text{attachFin}$ is a function that attaches a proof to each element in the interval that it is indeed a valid element of $\text{Fin}(n)$, and $\text{Ico}(a, b)$ denotes the set $\{x \in \text{Fin}(n) \mid a \leq x < b\}$.

Fin.attachFin_Ioc theorem

: attachFin (Ioc a b) (fun _x hx ↦ (mem_Ioc.mp hx).2.trans_lt b.2) = Ioc a b

Full source

@[simp]
theorem attachFin_Ioc :
    attachFin (Ioc a b) (fun _x hx ↦ (mem_Ioc.mp hx).2.trans_lt b.2) = Ioc a b :=
  rfl

$\text{attachFin}$ Preserves Open-Closed Interval in $\text{Fin}(n)$

Informal description

For any elements $a, b$ in $\text{Fin}(n)$, the operation $\text{attachFin}$ applied to the open-closed interval $\text{Ioc}(a, b)$ (with a proof that all elements in the interval are less than $b$) yields the same interval $\text{Ioc}(a, b)$. Here, $\text{attachFin}$ is a function that attaches a proof to each element in the interval that it is indeed a valid element of $\text{Fin}(n)$, and $\text{Ioc}(a, b)$ denotes the set $\{x \in \text{Fin}(n) \mid a < x \leq b\}$.

Fin.attachFin_Ioo theorem

: attachFin (Ioo a b) (fun _x hx ↦ (mem_Ioo.mp hx).2.trans b.2) = Ioo a b

Full source

@[simp]
theorem attachFin_Ioo :
    attachFin (Ioo a b) (fun _x hx ↦ (mem_Ioo.mp hx).2.trans b.2) = Ioo a b :=
  rfl

$\text{attachFin}$ Preserves Open Interval in $\text{Fin}(n)$

Informal description

For any elements $a, b$ in $\text{Fin}(n)$, the operation $\text{attachFin}$ applied to the open interval $\text{Ioo}(a, b)$ (with a proof that all elements in the interval are less than $b$) yields the same interval $\text{Ioo}(a, b)$. Here, $\text{attachFin}$ is a function that attaches a proof to each element in the interval that it is indeed a valid element of $\text{Fin}(n)$, and $\text{Ioo}(a, b)$ denotes the set $\{x \in \text{Fin}(n) \mid a < x < b\}$.

Fin.attachFin_uIcc theorem

: attachFin (uIcc a b) (fun _x hx ↦ (mem_Icc.mp hx).2.trans_lt (max a b).2) = uIcc a b

Full source

@[simp]
theorem attachFin_uIcc :
    attachFin (uIcc a b) (fun _x hx ↦ (mem_Icc.mp hx).2.trans_lt (max a b).2) = uIcc a b :=
  rfl

$\text{attachFin}$ Preserves Unordered Closed Interval in $\text{Fin}(n)$

Informal description

For any elements $a, b$ in $\text{Fin}(n)$, the operation $\text{attachFin}$ applied to the unordered closed interval $\text{uIcc}(a, b)$ (with a proof that all elements in the interval are less than the maximum of $a$ and $b$) yields the same interval $\text{uIcc}(a, b)$. Here, $\text{uIcc}(a, b)$ denotes the set $\{x \in \text{Fin}(n) \mid \min(a, b) \leq x \leq \max(a, b)\}$.

Fin.attachFin_Ico_eq_Ici theorem

: attachFin (Ico a n) (fun _x hx ↦ (mem_Ico.mp hx).2) = Ici a

Full source

@[simp]
theorem attachFin_Ico_eq_Ici : attachFin (Ico a n) (fun _x hx ↦ (mem_Ico.mp hx).2) = Ici a := by
  ext; simp

$\text{attachFin}$ Maps $\text{Ico}(a, n)$ to $\text{Ici}(a)$ in $\text{Fin}(n)$

Informal description

For any element $a$ in $\text{Fin}(n)$, the operation $\text{attachFin}$ applied to the closed-open interval $\text{Ico}(a, n)$ (with a proof that all elements in the interval are less than $n$) yields the same set as the closed-infinite interval $\text{Ici}(a)$. Here, $\text{Ico}(a, n)$ denotes the set $\{x \in \text{Fin}(n) \mid a \leq x < n\}$ and $\text{Ici}(a)$ denotes the set $\{x \in \text{Fin}(n) \mid a \leq x\}$.

Fin.attachFin_Ioo_eq_Ioi theorem

: attachFin (Ioo a n) (fun _x hx ↦ (mem_Ioo.mp hx).2) = Ioi a

Full source

@[simp]
theorem attachFin_Ioo_eq_Ioi : attachFin (Ioo a n) (fun _x hx ↦ (mem_Ioo.mp hx).2) = Ioi a := by
  ext; simp

$\text{attachFin}$ Maps Open Interval to Open Infinite Interval in $\text{Fin}(n)$

Informal description

For any element $a$ in $\text{Fin}(n)$, the operation $\text{attachFin}$ applied to the open interval $\text{Ioo}(a, n)$ (with a proof that all elements in the interval are less than $n$) yields the open infinite interval $\text{Ioi}(a)$. Here, $\text{Ioo}(a, n)$ denotes the set $\{x \in \text{Fin}(n) \mid a < x < n\}$ and $\text{Ioi}(a)$ denotes the set $\{x \in \text{Fin}(n) \mid a < x\}$.

Fin.attachFin_Iic theorem

: attachFin (Iic a) (fun _x hx ↦ (mem_Iic.mp hx).trans_lt a.2) = Iic a

Full source

@[simp]
theorem attachFin_Iic : attachFin (Iic a) (fun _x hx ↦ (mem_Iic.mp hx).trans_lt a.2) = Iic a := by
  ext; simp

Subtype Construction Preserves Closed Lower Interval in $\text{Fin}(n)$

Informal description

For any element $a$ in $\text{Fin}(n)$, the finset obtained by attaching the proof that each element in the closed lower interval $\text{Iic}(a)$ is less than $n$ is equal to $\text{Iic}(a)$ itself. In other words, the subtype construction of $\text{Iic}(a)$ preserving the bound $a.2$ yields the same finset as $\text{Iic}(a)$.

Fin.attachFin_Iio theorem

: attachFin (Iio a) (fun _x hx ↦ (mem_Iio.mp hx).trans a.2) = Iio a

Full source

@[simp]
theorem attachFin_Iio : attachFin (Iio a) (fun _x hx ↦ (mem_Iio.mp hx).trans a.2) = Iio a := by
  ext; simp

Equality of Attached Open Lower Interval in $\text{Fin}(n)$

Informal description

For any element $a$ in $\text{Fin}(n)$, the finset obtained by attaching the proof that each element in the open lower interval $\text{Iio}(a)$ is less than $n$ is equal to $\text{Iio}(a)$ itself. That is, $\text{attachFin}(\text{Iio}(a), \lambda x hx, (hx : x < a) \leq a.2) = \text{Iio}(a)$.

Fin.Icc_eq_finset_subtype theorem

: Icc a b = (Icc (a : ℕ) b).fin n

Full source

@[deprecated attachFin_Icc (since := "2025-04-06")]
theorem Icc_eq_finset_subtype : Icc a b = (Icc (a : ℕ) b).fin n := attachFin_eq_fin _

Closed Interval in $\text{Fin}(n)$ as Subtype of Natural Numbers Interval

Informal description

For any two elements $a, b$ in $\text{Fin}(n)$, the closed interval $[a, b]$ in $\text{Fin}(n)$ is equal to the finset obtained by taking the closed interval $[a, b]$ in $\mathbb{N}$ and restricting it to elements less than $n$.

Fin.Ico_eq_finset_subtype theorem

: Ico a b = (Ico (a : ℕ) b).fin n

Full source

@[deprecated attachFin_Ico (since := "2025-04-06")]
theorem Ico_eq_finset_subtype : Ico a b = (Ico (a : ℕ) b).fin n := attachFin_eq_fin _

Half-open Interval in $\text{Fin}(n)$ as Subset of Natural Numbers Interval

Informal description

For any two elements $a, b$ in $\text{Fin}(n)$, the half-open interval $[a, b)$ in $\text{Fin}(n)$ is equal to the finset obtained by taking the half-open interval $[a, b)$ in $\mathbb{N}$ and restricting it to elements less than $n$.

Fin.Ioc_eq_finset_subtype theorem

: Ioc a b = (Ioc (a : ℕ) b).fin n

Full source

@[deprecated attachFin_Ioc (since := "2025-04-06")]
theorem Ioc_eq_finset_subtype : Ioc a b = (Ioc (a : ℕ) b).fin n := attachFin_eq_fin _

Open-Closed Interval in $\text{Fin}(n)$ as Subset of Natural Numbers Interval

Informal description

For any two elements $a, b$ in $\text{Fin}(n)$, the open-closed interval $(a, b]$ in $\text{Fin}(n)$ is equal to the finset obtained by taking the open-closed interval $(a, b]$ in $\mathbb{N}$ and restricting it to elements less than $n$.

Fin.Ioo_eq_finset_subtype theorem

: Ioo a b = (Ioo (a : ℕ) b).fin n

Full source

@[deprecated attachFin_Ioo (since := "2025-04-06")]
theorem Ioo_eq_finset_subtype : Ioo a b = (Ioo (a : ℕ) b).fin n := attachFin_eq_fin _

Open Interval in $\text{Fin}(n)$ as Subset of Natural Numbers Interval

Informal description

For any two elements $a, b$ in $\text{Fin}(n)$, the open interval $(a, b)$ in $\text{Fin}(n)$ is equal to the finset obtained by taking the open interval $(a, b)$ in $\mathbb{N}$ and restricting it to elements less than $n$.

Fin.uIcc_eq_finset_subtype theorem

: uIcc a b = (uIcc (a : ℕ) b).fin n

Full source

@[deprecated attachFin_uIcc (since := "2025-04-06")]
theorem uIcc_eq_finset_subtype : uIcc a b = (uIcc (a : ℕ) b).fin n := Icc_eq_finset_subtype _ _

Unordered Closed Interval in $\text{Fin}(n)$ as Subset of Natural Numbers Interval

Informal description

For any two elements $a, b$ in $\text{Fin}(n)$, the unordered closed interval $\text{uIcc}(a, b)$ in $\text{Fin}(n)$ is equal to the finset obtained by taking the unordered closed interval $\text{uIcc}(a, b)$ in $\mathbb{N}$ and restricting it to elements less than $n$.

Fin.Ici_eq_finset_subtype theorem

: Ici a = (Ico (a : ℕ) n).fin n

Full source

@[deprecated attachFin_Ico_eq_Ici (since := "2025-04-06")]
theorem Ici_eq_finset_subtype : Ici a = (Ico (a : ℕ) n).fin n := by ext; simp

Closed-Infinite Interval in $\text{Fin}(n)$ as Subset of Natural Numbers Interval

Informal description

For any element $a$ in $\text{Fin}(n)$, the closed-infinite interval $[a, \top]$ in $\text{Fin}(n)$ is equal to the finset obtained by taking the closed-open interval $[a, n)$ in $\mathbb{N}$ and restricting it to elements less than $n$.

Fin.Ioi_eq_finset_subtype theorem

: Ioi a = (Ioo (a : ℕ) n).fin n

Full source

@[deprecated attachFin_Ioo_eq_Ioi (since := "2025-04-06")]
theorem Ioi_eq_finset_subtype : Ioi a = (Ioo (a : ℕ) n).fin n := by ext; simp

Open Infinite Interval in $\text{Fin}(n)$ as Subset of Natural Numbers Interval

Informal description

For any element $a$ in $\text{Fin}(n)$, the open infinite interval $\text{Ioi}(a)$ (elements greater than $a$) is equal to the finset obtained by taking the open interval $(a, n)$ in $\mathbb{N}$ and restricting it to elements of $\text{Fin}(n)$.

Fin.Iic_eq_finset_subtype theorem

: Iic b = (Iic (b : ℕ)).fin n

Full source

@[deprecated attachFin_Iic (since := "2025-04-06")]
theorem Iic_eq_finset_subtype : Iic b = (Iic (b : ℕ)).fin n := by ext; simp

Lower-Closed Interval in $\text{Fin}(n)$ as Subset of Natural Numbers

Informal description

For any natural number $n$ and any element $b \in \text{Fin}(n)$, the lower-closed interval $\text{Iic}(b)$ in $\text{Fin}(n)$ is equal to the finset obtained by restricting the natural number interval $\text{Iic}(b)$ (viewed as a subset of $\mathbb{N}$) back to $\text{Fin}(n)$. More precisely, $\text{Iic}(b) = \{x \in \text{Fin}(n) \mid x \leq b\} = \{k \in \mathbb{N} \mid k \leq b\} \cap \text{Fin}(n)$.

Fin.Iio_eq_finset_subtype theorem

: Iio b = (Iio (b : ℕ)).fin n

Full source

@[deprecated attachFin_Iio (since := "2025-04-06")]
theorem Iio_eq_finset_subtype : Iio b = (Iio (b : ℕ)).fin n := by ext; simp

Open Lower Interval in $\text{Fin}(n)$ as Restriction from $\mathbb{N}$

Informal description

For any element $b$ in $\text{Fin}(n)$, the open lower interval $\text{Iio}(b)$ (consisting of all elements less than $b$) is equal to the finset obtained by taking the open lower interval $\text{Iio}(b)$ in $\mathbb{N}$ (where $b$ is interpreted as a natural number) and restricting it to $\text{Fin}(n)$ via the `.fin n` operation.

Fin.finsetImage_val_Icc theorem

: (Icc a b).image val = Icc (a : ℕ) b

Full source

@[simp]
theorem finsetImage_val_Icc : (Icc a b).image val = Icc (a : ℕ) b :=
  image_val_attachFin _

Image of Closed Interval in $\text{Fin}(n)$ under Natural Embedding Equals Closed Interval in $\mathbb{N}$

Informal description

For any elements $a, b$ in $\text{Fin}(n)$, the image of the closed interval $[a, b]$ under the natural embedding $\text{val} : \text{Fin}(n) \to \mathbb{N}$ is equal to the closed interval $[a, b]$ in $\mathbb{N}$ (where $a$ and $b$ are interpreted as natural numbers).

Fin.finsetImage_val_Ico theorem

: (Ico a b).image val = Ico (a : ℕ) b

Full source

@[simp]
theorem finsetImage_val_Ico : (Ico a b).image val = Ico (a : ℕ) b :=
  image_val_attachFin _

Image of Closed-Open Interval in $\text{Fin}(n)$ under Natural Embedding Equals Closed-Open Interval in $\mathbb{N}$

Informal description

For any elements $a, b$ in $\text{Fin}(n)$, the image of the closed-open interval $[a, b)$ under the natural embedding $\text{val} : \text{Fin}(n) \to \mathbb{N}$ is equal to the closed-open interval $[a, b)$ in $\mathbb{N}$ (where $a$ and $b$ are interpreted as natural numbers).

Fin.finsetImage_val_Ioc theorem

: (Ioc a b).image val = Ioc (a : ℕ) b

Full source

@[simp]
theorem finsetImage_val_Ioc : (Ioc a b).image val = Ioc (a : ℕ) b :=
  image_val_attachFin _

Image of Open-Closed Interval in $\text{Fin}(n)$ under Natural Embedding Equals Open-Closed Interval in $\mathbb{N}$

Informal description

For any elements $a, b$ in $\text{Fin}(n)$, the image of the open-closed interval $(a, b]$ under the natural embedding $\text{val} : \text{Fin}(n) \to \mathbb{N}$ is equal to the open-closed interval $(a, b]$ in $\mathbb{N}$ (where $a$ and $b$ are interpreted as natural numbers).

Fin.finsetImage_val_Ioo theorem

: (Ioo a b).image val = Ioo (a : ℕ) b

Full source

@[simp]
theorem finsetImage_val_Ioo : (Ioo a b).image val = Ioo (a : ℕ) b :=
  image_val_attachFin _

Image of Open Interval in $\text{Fin}(n)$ under Natural Embedding Equals Open Interval in $\mathbb{N}$

Informal description

For any elements $a, b$ in $\text{Fin}(n)$, the image of the open interval $(a, b)$ under the natural embedding $\text{val} : \text{Fin}(n) \to \mathbb{N}$ is equal to the open interval $(a, b)$ in $\mathbb{N}$ (where $a$ and $b$ are interpreted as natural numbers).

Fin.finsetImage_val_uIcc theorem

: (uIcc a b).image val = uIcc (a : ℕ) b

Full source

@[simp]
theorem finsetImage_val_uIcc : (uIcc a b).image val = uIcc (a : ℕ) b :=
  finsetImage_val_Icc _ _

Image of Unordered Closed Interval in $\text{Fin}(n)$ under Natural Embedding Equals Unordered Closed Interval in $\mathbb{N}$

Informal description

For any elements $a, b$ in $\text{Fin}(n)$, the image of the unordered closed interval $\text{uIcc}(a, b)$ under the natural embedding $\text{val} : \text{Fin}(n) \to \mathbb{N}$ is equal to the unordered closed interval $\text{uIcc}(a, b)$ in $\mathbb{N}$ (where $a$ and $b$ are interpreted as natural numbers).

Fin.finsetImage_val_Ici theorem

: (Ici a).image val = Ico (a : ℕ) n

Full source

@[simp]
theorem finsetImage_val_Ici : (Ici a).image val = Ico (a : ℕ) n := by simp [← coe_inj]

Image of $[a, \infty)$ under Fin.val equals $[a, n)$

Informal description

For any element $a$ in $\text{Fin}(n)$, the image of the closed-infinite interval $[a, \infty)$ under the natural embedding $\text{val} : \text{Fin}(n) \to \mathbb{N}$ is equal to the closed-open interval $[a, n)$ in $\mathbb{N}$. In symbols: $$ \text{val}([a, \infty)) = [a, n) $$ where $\text{val}$ denotes the natural embedding from $\text{Fin}(n)$ to $\mathbb{N}$.

Fin.finsetImage_val_Ioi theorem

: (Ioi a).image val = Ioo (a : ℕ) n

Full source

@[simp]
theorem finsetImage_val_Ioi : (Ioi a).image val = Ioo (a : ℕ) n := by simp [← coe_inj]

Image of Right-Infinite Interval under Fin.val Embedding Equals Open Interval

Informal description

For any element $a$ in the finite type $\text{Fin}\,n$, the image of the left-open right-infinite interval $(a, \infty)$ under the canonical embedding $\text{Fin}\,n \to \mathbb{N}$ is equal to the open interval $(a, n)$ in $\mathbb{N}$.

Fin.finsetImage_val_Iic theorem

: (Iic a).image val = Iic (a : ℕ)

Full source

@[simp]
theorem finsetImage_val_Iic : (Iic a).image val = Iic (a : ℕ) := by simp [← coe_inj]

Image of Lower-Closed Interval under Natural Coercion: $\text{val}(\text{Iic}(a)) = \text{Iic}(a)$ in $\mathbb{N}$

Informal description

For any element $a$ in the finite type $\text{Fin } n$, the image of the lower-closed interval $(-\infty, a]$ under the natural coercion map $\text{Fin } n \to \mathbb{N}$ is equal to the lower-closed interval $(-\infty, a]$ in $\mathbb{N}$, where $a$ is interpreted as a natural number.

Fin.finsetImage_val_Iio theorem

: (Iio b).image val = Iio (b : ℕ)

Full source

@[simp]
theorem finsetImage_val_Iio : (Iio b).image val = Iio (b : ℕ) := by simp [← coe_inj]

Natural Coercion Preserves Open Lower Intervals from $\text{Fin}(n)$ to $\mathbb{N}$

Informal description

For any element $b$ in $\text{Fin}(n)$, the image of the open lower interval $(-\infty, b)$ under the natural coercion map $\text{val} : \text{Fin}(n) \to \mathbb{N}$ is equal to the open lower interval $(-\infty, \text{val}(b))$ in $\mathbb{N}$. In symbols: $$\text{val}\big((-\infty, b)\big) = (-\infty, \text{val}(b))$$

Fin.map_valEmbedding_Icc theorem

: (Icc a b).map Fin.valEmbedding = Icc (a : ℕ) b

Full source

@[simp]
theorem map_valEmbedding_Icc : (Icc a b).map Fin.valEmbedding = Icc (a : ℕ) b :=
  map_valEmbedding_attachFin _

Natural Embedding Preserves Closed Intervals in Finite Types

Informal description

For any two elements $a, b$ in $\text{Fin}(n)$, the image of the closed interval $[a, b]$ under the natural embedding $\text{val} : \text{Fin}(n) \to \mathbb{N}$ is equal to the closed interval $[a, b]$ in $\mathbb{N}$, where $a$ and $b$ are interpreted as natural numbers.

Fin.map_valEmbedding_Ico theorem

: (Ico a b).map Fin.valEmbedding = Ico (a : ℕ) b

Full source

@[simp]
theorem map_valEmbedding_Ico : (Ico a b).map Fin.valEmbedding = Ico (a : ℕ) b :=
  map_valEmbedding_attachFin _

Natural Embedding Preserves Half-Open Intervals from $\text{Fin}(n)$ to $\mathbb{N}$

Informal description

For any two elements $a, b$ in $\text{Fin}(n)$, the image of the half-open interval $[a, b)$ under the natural embedding $\text{val} : \text{Fin}(n) \to \mathbb{N}$ is equal to the half-open interval $[a, b)$ in $\mathbb{N}$, where $a$ and $b$ are interpreted as natural numbers.

Fin.map_valEmbedding_Ioc theorem

: (Ioc a b).map Fin.valEmbedding = Ioc (a : ℕ) b

Full source

@[simp]
theorem map_valEmbedding_Ioc : (Ioc a b).map Fin.valEmbedding = Ioc (a : ℕ) b :=
  map_valEmbedding_attachFin _

Natural Embedding Preserves Open-Closed Intervals from $\text{Fin}(n)$ to $\mathbb{N}$

Informal description

For any two elements $a, b$ in $\text{Fin}(n)$, the image of the open-closed interval $(a, b]$ under the natural embedding $\text{val} : \text{Fin}(n) \to \mathbb{N}$ is equal to the open-closed interval $(a, b]$ in $\mathbb{N}$, where $a$ and $b$ are interpreted as natural numbers.

Fin.map_valEmbedding_Ioo theorem

: (Ioo a b).map Fin.valEmbedding = Ioo (a : ℕ) b

Full source

@[simp]
theorem map_valEmbedding_Ioo : (Ioo a b).map Fin.valEmbedding = Ioo (a : ℕ) b :=
  map_valEmbedding_attachFin _

Embedding Preserves Open Intervals from $\text{Fin}(n)$ to $\mathbb{N}$

Informal description

For any two elements $a, b$ in $\text{Fin}(n)$, the image of the open interval $(a, b)$ under the embedding $\text{Fin.valEmbedding} : \text{Fin}(n) \to \mathbb{N}$ is equal to the open interval $(a, b)$ in $\mathbb{N}$.

Fin.map_valEmbedding_uIcc theorem

: (uIcc a b).map valEmbedding = uIcc (a : ℕ) b

Full source

@[simp]
theorem map_valEmbedding_uIcc : (uIcc a b).map valEmbedding = uIcc (a : ℕ) b :=
  map_valEmbedding_Icc _ _

Natural Embedding Preserves Unordered Closed Intervals from $\text{Fin}(n)$ to $\mathbb{N}$

Informal description

For any two elements $a, b$ in $\text{Fin}(n)$, the image of the unordered closed interval $\text{uIcc}(a, b)$ under the natural embedding $\text{val} : \text{Fin}(n) \to \mathbb{N}$ is equal to the unordered closed interval $\text{uIcc}(a, b)$ in $\mathbb{N}$, where $a$ and $b$ are interpreted as natural numbers.

Fin.map_valEmbedding_Ici theorem

: (Ici a).map Fin.valEmbedding = Ico (a : ℕ) n

Full source

@[simp]
theorem map_valEmbedding_Ici : (Ici a).map Fin.valEmbedding = Ico (a : ℕ) n := by
  rw [← attachFin_Ico_eq_Ici, map_valEmbedding_attachFin]

Embedding Maps Closed-Infinite Interval in $\text{Fin}(n)$ to Closed-Open Interval in $\mathbb{N}$

Informal description

For any element $a$ in $\text{Fin}(n)$, the image of the closed-infinite interval $\text{Ici}(a) = \{x \in \text{Fin}(n) \mid a \leq x\}$ under the natural embedding $\text{val} : \text{Fin}(n) \to \mathbb{N}$ is equal to the closed-open interval $\text{Ico}(a, n) = \{x \in \mathbb{N} \mid a \leq x < n\}$ in $\mathbb{N}$.

Fin.map_valEmbedding_Ioi theorem

: (Ioi a).map Fin.valEmbedding = Ioo (a : ℕ) n

Full source

@[simp]
theorem map_valEmbedding_Ioi : (Ioi a).map Fin.valEmbedding = Ioo (a : ℕ) n := by
  rw [← attachFin_Ioo_eq_Ioi, map_valEmbedding_attachFin]

Natural Embedding Maps Open Infinite Interval in $\text{Fin}(n)$ to Open Interval in $\mathbb{N}$

Informal description

For any element $a$ in $\text{Fin}(n)$, the image of the open infinite interval $\text{Ioi}(a) = \{x \in \text{Fin}(n) \mid a < x\}$ under the natural embedding $\text{val} : \text{Fin}(n) \to \mathbb{N}$ is equal to the open interval $\text{Ioo}(a, n) = \{k \in \mathbb{N} \mid a < k < n\}$ in $\mathbb{N}$.

Fin.map_valEmbedding_Iic theorem

: (Iic a).map Fin.valEmbedding = Iic (a : ℕ)

Full source

@[simp]
theorem map_valEmbedding_Iic : (Iic a).map Fin.valEmbedding = Iic (a : ℕ) := by
  rw [← attachFin_Iic, map_valEmbedding_attachFin]

Image of Closed Lower Interval in $\text{Fin}(n)$ under Natural Embedding Equals Closed Lower Interval in $\mathbb{N}$

Informal description

For any element $a$ in $\text{Fin}(n)$, the image of the closed lower interval $\text{Iic}(a) = \{x \in \text{Fin}(n) \mid x \leq a\}$ under the embedding $\text{Fin.valEmbedding} : \text{Fin}(n) \to \mathbb{N}$ is equal to the closed lower interval $\text{Iic}(a) = \{k \in \mathbb{N} \mid k \leq a\}$ in $\mathbb{N}$.

Fin.map_valEmbedding_Iio theorem

: (Iio a).map Fin.valEmbedding = Iio (a : ℕ)

Full source

@[simp]
theorem map_valEmbedding_Iio : (Iio a).map Fin.valEmbedding = Iio (a : ℕ) := by
  rw [← attachFin_Iio, map_valEmbedding_attachFin]

Embedding Preserves Open Lower Interval: $\text{valEmbedding}(\text{Iio}(a)) = \text{Iio}(a)$ in $\mathbb{N}$

Informal description

For any element $a$ in $\text{Fin}(n)$, the image of the open lower interval $\text{Iio}(a)$ under the embedding $\text{Fin.valEmbedding} : \text{Fin}(n) \to \mathbb{N}$ is equal to the open lower interval $\text{Iio}(a)$ in $\mathbb{N}$, where $a$ is viewed as a natural number. That is, $\text{valEmbedding}(\text{Iio}(a)) = \{x \in \mathbb{N} \mid x < a\}$.

Fin.finsetImage_castLE_Icc theorem

(h : n ≤ m) : (Icc a b).image (castLE h) = Icc (castLE h a) (castLE h b)

Full source

@[simp]
theorem finsetImage_castLE_Icc (h : n ≤ m) :
    (Icc a b).image (castLE h) = Icc (castLE h a) (castLE h b) := by simp [← coe_inj]

Image of Closed Interval under Order-Preserving Embedding $\text{castLE}$ Equals Closed Interval in Target

Informal description

For any natural numbers $n$ and $m$ with $n \leq m$, and for any elements $a, b \in \text{Fin}\,n$, the image of the closed interval $[a, b]$ under the order-preserving embedding $\text{castLE}\,h : \text{Fin}\,n \to \text{Fin}\,m$ is equal to the closed interval $[\text{castLE}\,h\,a, \text{castLE}\,h\,b]$ in $\text{Fin}\,m$.

Fin.finsetImage_castLE_Ico theorem

(h : n ≤ m) : (Ico a b).image (castLE h) = Ico (castLE h a) (castLE h b)

Full source

@[simp]
theorem finsetImage_castLE_Ico (h : n ≤ m) :
    (Ico a b).image (castLE h) = Ico (castLE h a) (castLE h b) := by simp [← coe_inj]

Image of $[a, b)$ under $\text{castLE}\,h$ equals $[\text{castLE}\,h\,a, \text{castLE}\,h\,b)$ in $\text{Fin}(m)$

Informal description

For any natural numbers $n$ and $m$ with $n \leq m$, and for any elements $a, b \in \text{Fin}(n)$, the image of the closed-open interval $[a, b)$ under the order-preserving embedding $\text{castLE}\,h : \text{Fin}(n) \to \text{Fin}(m)$ is equal to the closed-open interval $[\text{castLE}\,h\,a, \text{castLE}\,h\,b)$ in $\text{Fin}(m)$.

Fin.finsetImage_castLE_Ioc theorem

(h : n ≤ m) : (Ioc a b).image (castLE h) = Ioc (castLE h a) (castLE h b)

Full source

@[simp]
theorem finsetImage_castLE_Ioc (h : n ≤ m) :
    (Ioc a b).image (castLE h) = Ioc (castLE h a) (castLE h b) := by simp [← coe_inj]

Image of Open-Closed Interval under Order-Preserving Embedding in Finite Types

Informal description

For any natural numbers $n$ and $m$ with $n \leq m$, and for any elements $a, b \in \text{Fin}(n)$, the image of the left-open right-closed interval $(a, b]$ under the order-preserving embedding $\text{castLE}\,h$ is equal to the left-open right-closed interval $(\text{castLE}\,h\,a, \text{castLE}\,h\,b]$ in $\text{Fin}(m)$.

Fin.finsetImage_castLE_Ioo theorem

(h : n ≤ m) : (Ioo a b).image (castLE h) = Ioo (castLE h a) (castLE h b)

Full source

@[simp]
theorem finsetImage_castLE_Ioo (h : n ≤ m) :
    (Ioo a b).image (castLE h) = Ioo (castLE h a) (castLE h b) := by simp [← coe_inj]

Image of Open Interval Finset under Order-Preserving Embedding Equals Open Interval Finset in Target Type

Informal description

For any natural numbers $n$ and $m$ with $n \leq m$, and for any elements $a, b \in \text{Fin}(n)$, the image of the open interval finset $\text{Ioo}(a, b)$ under the order-preserving embedding $\text{castLE}\,h$ is equal to the open interval finset $\text{Ioo}(\text{castLE}\,h\,a, \text{castLE}\,h\,b)$ in $\text{Fin}(m)$.

Fin.finsetImage_castLE_uIcc theorem

(h : n ≤ m) : (uIcc a b).image (castLE h) = uIcc (castLE h a) (castLE h b)

Full source

@[simp]
theorem finsetImage_castLE_uIcc (h : n ≤ m) :
    (uIcc a b).image (castLE h) = uIcc (castLE h a) (castLE h b) := by simp [← coe_inj]

Image of Unordered Closed Interval under Order-Preserving Embedding in Finite Types

Informal description

For any natural numbers $n$ and $m$ with $n \leq m$, and for any elements $a, b \in \text{Fin}(n)$, the image of the unordered closed interval $\text{uIcc}(a, b)$ under the order-preserving embedding $\text{castLE}\,h : \text{Fin}(n) \to \text{Fin}(m)$ is equal to the unordered closed interval $\text{uIcc}(\text{castLE}\,h\,a, \text{castLE}\,h\,b)$ in $\text{Fin}(m)$.

Fin.finsetImage_castLE_Iic theorem

(h : n ≤ m) : (Iic a).image (castLE h) = Iic (castLE h a)

Full source

@[simp]
theorem finsetImage_castLE_Iic (h : n ≤ m) :
    (Iic a).image (castLE h) = Iic (castLE h a) := by simp [← coe_inj]

Image of Lower-Closed Interval under Order-Preserving Embedding in Finite Types

Informal description

For natural numbers $n$ and $m$ with $n \leq m$, and for any element $a \in \text{Fin}(n)$, the image of the lower-closed interval $(-\infty, a]$ under the order-preserving embedding $\text{castLE}\ h : \text{Fin}(n) \to \text{Fin}(m)$ is equal to the lower-closed interval $(-\infty, \text{castLE}\ h\ a]$ in $\text{Fin}(m)$. In symbols: $$\text{castLE}\ h\big((-\infty, a]\big) = (-\infty, \text{castLE}\ h\ a]$$

Fin.finsetImage_castLE_Iio theorem

(h : n ≤ m) : (Iio a).image (castLE h) = Iio (castLE h a)

Full source

@[simp]
theorem finsetImage_castLE_Iio (h : n ≤ m) :
    (Iio a).image (castLE h) = Iio (castLE h a) := by simp [← coe_inj]

Image of Open Lower Interval under $\text{Fin.castLE}$ Equals Open Lower Interval of Image

Informal description

For any natural numbers $n$ and $m$ with $n \leq m$, and for any element $a \in \text{Fin}(n)$, the image of the open lower interval $(-\infty, a)$ under the order-preserving embedding $\text{castLE}\ h : \text{Fin}(n) \to \text{Fin}(m)$ is equal to the open lower interval $(-\infty, \text{castLE}\ h\ a)$ in $\text{Fin}(m)$. In symbols: $$\text{castLE}\ h\big((-\infty, a)\big) = (-\infty, \text{castLE}\ h\ a)$$

Fin.map_castLEEmb_Icc theorem

(h : n ≤ m) : (Icc a b).map (castLEEmb h) = Icc (castLE h a) (castLE h b)

Full source

@[simp]
theorem map_castLEEmb_Icc (h : n ≤ m) :
    (Icc a b).map (castLEEmb h) = Icc (castLE h a) (castLE h b) := by simp [← coe_inj]

Image of Closed Interval under $\text{castLEEmb}$ Equals Closed Interval in Target

Informal description

For any natural numbers $n$ and $m$ with $n \leq m$, and for any elements $a, b \in \text{Fin}\,n$, the image of the closed interval $[a, b]$ under the order-preserving embedding $\text{castLEEmb}\,h : \text{Fin}\,n \to \text{Fin}\,m$ is equal to the closed interval $[\text{castLE}\,h\,a, \text{castLE}\,h\,b]$ in $\text{Fin}\,m$.

Fin.map_castLEEmb_Ico theorem

(h : n ≤ m) : (Ico a b).map (castLEEmb h) = Ico (castLE h a) (castLE h b)

Full source

@[simp]
theorem map_castLEEmb_Ico (h : n ≤ m) :
    (Ico a b).map (castLEEmb h) = Ico (castLE h a) (castLE h b) := by simp [← coe_inj]

Image of $[a, b)$ under $\text{castLEEmb}\,h$ equals $[\text{castLE}\,h\,a, \text{castLE}\,h\,b)$ in $\text{Fin}(m)$

Informal description

For any natural numbers $n$ and $m$ with $n \leq m$, and for any elements $a, b \in \text{Fin}(n)$, the image of the closed-open interval $[a, b)$ under the order-preserving embedding $\text{castLEEmb}\,h : \text{Fin}(n) \to \text{Fin}(m)$ is equal to the closed-open interval $[\text{castLE}\,h\,a, \text{castLE}\,h\,b)$ in $\text{Fin}(m)$.

Fin.map_castLEEmb_Ioc theorem

(h : n ≤ m) : (Ioc a b).map (castLEEmb h) = Ioc (castLE h a) (castLE h b)

Full source

@[simp]
theorem map_castLEEmb_Ioc (h : n ≤ m) :
    (Ioc a b).map (castLEEmb h) = Ioc (castLE h a) (castLE h b) := by simp [← coe_inj]

Image of Open-Closed Interval under Order-Preserving Embedding Equals Open-Closed Interval in Target Type

Informal description

For any natural numbers $n$ and $m$ with $n \leq m$, and for any elements $a, b \in \text{Fin}(n)$, the image of the left-open right-closed interval $(a, b]$ under the order-preserving embedding $\text{castLEEmb}\,h$ is equal to the left-open right-closed interval $(\text{castLE}\,h\,a, \text{castLE}\,h\,b]$ in $\text{Fin}(m)$.

Fin.map_castLEEmb_Ioo theorem

(h : n ≤ m) : (Ioo a b).map (castLEEmb h) = Ioo (castLE h a) (castLE h b)

Full source

@[simp]
theorem map_castLEEmb_Ioo (h : n ≤ m) :
    (Ioo a b).map (castLEEmb h) = Ioo (castLE h a) (castLE h b) := by simp [← coe_inj]

Image of Open Interval under Order-Preserving Embedding Equals Open Interval in Target Type

Informal description

For any natural numbers $n$ and $m$ with $n \leq m$, and for any elements $a, b \in \text{Fin}\,n$, the image of the open interval $(a, b)$ under the order-preserving embedding $\text{castLEEmb}\,h$ is equal to the open interval $(\text{castLE}\,h\,a, \text{castLE}\,h\,b)$ in $\text{Fin}\,m$.

Fin.map_castLEEmb_uIcc theorem

(h : n ≤ m) : (uIcc a b).map (castLEEmb h) = uIcc (castLE h a) (castLE h b)

Full source

@[simp]
theorem map_castLEEmb_uIcc (h : n ≤ m) :
    (uIcc a b).map (castLEEmb h) = uIcc (castLE h a) (castLE h b) := by simp [← coe_inj]

Image of Unordered Closed Interval under Order-Preserving Embedding Equals Unordered Closed Interval in Target

Informal description

For natural numbers $n$ and $m$ with $n \leq m$, and for any elements $a, b \in \text{Fin}(n)$, the image of the unordered closed interval $\text{uIcc}(a, b)$ under the order-preserving embedding $\text{castLEEmb}\ h : \text{Fin}(n) \to \text{Fin}(m)$ is equal to the unordered closed interval $\text{uIcc}(\text{castLE}\ h\ a, \text{castLE}\ h\ b)$ in $\text{Fin}(m)$. In symbols: $$\text{castLEEmb}\ h\big(\text{uIcc}(a, b)\big) = \text{uIcc}(\text{castLE}\ h\ a, \text{castLE}\ h\ b)$$

Fin.map_castLEEmb_Iic theorem

(h : n ≤ m) : (Iic a).map (castLEEmb h) = Iic (castLE h a)

Full source

@[simp]
theorem map_castLEEmb_Iic (h : n ≤ m) :
    (Iic a).map (castLEEmb h) = Iic (castLE h a) := by simp [← coe_inj]

Image of Lower-Closed Interval under Order-Preserving Embedding Equals Lower-Closed Interval of Image

Informal description

For any natural numbers $n$ and $m$ with $n \leq m$, and for any element $a \in \text{Fin}(n)$, the image of the lower-closed interval $(-\infty, a]$ under the order-preserving embedding $\text{castLEEmb}\ h : \text{Fin}(n) \to \text{Fin}(m)$ is equal to the lower-closed interval $(-\infty, \text{castLE}\ h\ a]$ in $\text{Fin}(m)$. In symbols: $$\text{castLEEmb}\ h\big((-\infty, a]\big) = (-\infty, \text{castLE}\ h\ a]$$

Fin.map_castLEEmb_Iio theorem

(h : n ≤ m) : (Iio a).map (castLEEmb h) = Iio (castLE h a)

Full source

@[simp]
theorem map_castLEEmb_Iio (h : n ≤ m) :
    (Iio a).map (castLEEmb h) = Iio (castLE h a) := by simp [← coe_inj]

Image of Open Lower Interval under $\text{castLEEmb}$ Equals Open Lower Interval of Image

Informal description

For natural numbers $n$ and $m$ with $n \leq m$, and for any element $a \in \text{Fin}(n)$, the image of the open lower interval $(-\infty, a)$ under the order-preserving embedding $\text{castLEEmb}\ h : \text{Fin}(n) \to \text{Fin}(m)$ is equal to the open lower interval $(-\infty, \text{castLE}\ h\ a)$ in $\text{Fin}(m)$. In symbols: $$\text{castLEEmb}\ h\big((-\infty, a)\big) = (-\infty, \text{castLE}\ h\ a)$$

Fin.finsetImage_castAdd_Icc theorem

(m) (i j : Fin n) : (Icc i j).image (castAdd m) = Icc (castAdd m i) (castAdd m j)

Full source

@[simp]
theorem finsetImage_castAdd_Icc (m) (i j : Fin n) :
    (Icc i j).image (castAdd m) = Icc (castAdd m i) (castAdd m j) :=
  finsetImage_castLE_Icc ..

Image of Closed Interval under $\text{castAdd}$ Equals Closed Interval in Target

Informal description

For any natural number $m$ and elements $i, j \in \text{Fin}(n)$, the image of the closed interval $[i, j]$ under the embedding $\text{castAdd}\,m : \text{Fin}(n) \to \text{Fin}(n + m)$ is equal to the closed interval $[\text{castAdd}\,m\,i, \text{castAdd}\,m\,j]$ in $\text{Fin}(n + m)$.

Fin.finsetImage_castAdd_Ico theorem

(m) (i j : Fin n) : (Ico i j).image (castAdd m) = Ico (castAdd m i) (castAdd m j)

Full source

@[simp]
theorem finsetImage_castAdd_Ico (m) (i j : Fin n) :
    (Ico i j).image (castAdd m) = Ico (castAdd m i) (castAdd m j) :=
  finsetImage_castLE_Ico ..

Image of $[i, j)$ under $\text{castAdd}\,m$ equals $[\text{castAdd}\,m\,i, \text{castAdd}\,m\,j)$ in $\text{Fin}(n + m)$

Informal description

For any natural number $m$ and elements $i, j \in \text{Fin}(n)$, the image of the closed-open interval $[i, j)$ under the embedding $\text{castAdd}\,m : \text{Fin}(n) \to \text{Fin}(n + m)$ is equal to the closed-open interval $[\text{castAdd}\,m\,i, \text{castAdd}\,m\,j)$ in $\text{Fin}(n + m)$.

Fin.finsetImage_castAdd_Ioc theorem

(m) (i j : Fin n) : (Ioc i j).image (castAdd m) = Ioc (castAdd m i) (castAdd m j)

Full source

@[simp]
theorem finsetImage_castAdd_Ioc (m) (i j : Fin n) :
    (Ioc i j).image (castAdd m) = Ioc (castAdd m i) (castAdd m j) :=
  finsetImage_castLE_Ioc ..

Image of Open-Closed Interval under Order-Preserving Addition Embedding in Finite Types

Informal description

For any natural number $m$ and elements $i, j \in \text{Fin}(n)$, the image of the left-open right-closed interval $(i, j]$ under the order-preserving embedding $\text{castAdd}\,m$ is equal to the left-open right-closed interval $(\text{castAdd}\,m\,i, \text{castAdd}\,m\,j]$ in $\text{Fin}(n + m)$.

Fin.finsetImage_castAdd_Ioo theorem

(m) (i j : Fin n) : (Ioo i j).image (castAdd m) = Ioo (castAdd m i) (castAdd m j)

Full source

@[simp]
theorem finsetImage_castAdd_Ioo (m) (i j : Fin n) :
    (Ioo i j).image (castAdd m) = Ioo (castAdd m i) (castAdd m j) :=
  finsetImage_castLE_Ioo ..

Image of Open Interval under $\text{castAdd}$ Equals Open Interval in Extended Type

Informal description

For any natural number $m$ and any elements $i, j \in \text{Fin}(n)$, the image of the open interval finset $\text{Ioo}(i, j)$ under the embedding $\text{castAdd}\,m$ is equal to the open interval finset $\text{Ioo}(\text{castAdd}\,m\,i, \text{castAdd}\,m\,j)$ in $\text{Fin}(m + n)$.

Fin.finsetImage_castAdd_uIcc theorem

(m) (i j : Fin n) : (uIcc i j).image (castAdd m) = uIcc (castAdd m i) (castAdd m j)

Full source

@[simp]
theorem finsetImage_castAdd_uIcc (m) (i j : Fin n) :
    (uIcc i j).image (castAdd m) = uIcc (castAdd m i) (castAdd m j) :=
  finsetImage_castLE_uIcc ..

Image of Unordered Closed Interval under $\text{castAdd}$ Equals Unordered Closed Interval in Extended Type

Informal description

For any natural number $m$ and elements $i, j \in \text{Fin}(n)$, the image of the unordered closed interval $\text{uIcc}(i, j)$ under the embedding $\text{castAdd}\,m : \text{Fin}(n) \to \text{Fin}(m + n)$ is equal to the unordered closed interval $\text{uIcc}(\text{castAdd}\,m\,i, \text{castAdd}\,m\,j)$ in $\text{Fin}(m + n)$.

Fin.finsetImage_castAdd_Ici theorem

(m) [NeZero m] (i : Fin n) : (Ici i).image (castAdd m) = Ico (castAdd m i) (natAdd n 0)

Full source

@[simp]
theorem finsetImage_castAdd_Ici (m) [NeZero m] (i : Fin n) :
    (Ici i).image (castAdd m) = Ico (castAdd m i) (natAdd n 0) := by
  simp [← coe_inj]

Image of $[i, \infty)$ under $\text{castAdd}\,m$ equals $[\text{castAdd}\,m\,i, \text{natAdd}\,n\,0)$ in $\text{Fin}\,(m + n)$

Informal description

For any natural number $m \neq 0$ and any element $i$ in $\text{Fin}\,n$, the image of the left-closed right-infinite interval $[i, \infty)$ under the function $\text{castAdd}\,m$ is equal to the left-closed right-open interval $[\text{castAdd}\,m\,i, \text{natAdd}\,n\,0)$ in $\text{Fin}\,(m + n)$. In symbols: $$ \text{castAdd}\,m([i, \infty)) = [\text{castAdd}\,m\,i, \text{natAdd}\,n\,0) $$

Fin.finsetImage_castAdd_Ioi theorem

(m) [NeZero m] (i : Fin n) : (Ioi i).image (castAdd m) = Ioo (castAdd m i) (natAdd n 0)

Full source

@[simp]
theorem finsetImage_castAdd_Ioi (m) [NeZero m] (i : Fin n) :
    (Ioi i).image (castAdd m) = Ioo (castAdd m i) (natAdd n 0) := by
  simp [← coe_inj]

Image of Right-Infinite Interval under $\text{castAdd}\,m$ Equals Open Interval

Informal description

For any natural number $m \neq 0$ and any element $i$ in $\text{Fin}\,n$, the image of the open right-infinite interval $(i, \infty)$ under the function $\text{castAdd}\,m$ is equal to the open interval $(\text{castAdd}\,m\,i, \text{natAdd}\,n\,0)$ in $\text{Fin}\,(m + n)$. In symbols: $$ \text{castAdd}\,m\big((i, \infty)\big) = \big(\text{castAdd}\,m\,i, \text{natAdd}\,n\,0\big) $$

Fin.finsetImage_castAdd_Iic theorem

(m) (i : Fin n) : (Iic i).image (castAdd m) = Iic (castAdd m i)

Full source

@[simp]
theorem finsetImage_castAdd_Iic (m) (i : Fin n) : (Iic i).image (castAdd m) = Iic (castAdd m i) :=
  finsetImage_castLE_Iic i _

Image of Lower-Closed Interval under $\text{castAdd}\,m$ in Finite Types

Informal description

For any natural number $m$ and any element $i \in \text{Fin}(n)$, the image of the lower-closed interval $(-\infty, i]$ under the function $\text{castAdd}\,m : \text{Fin}(n) \to \text{Fin}(m + n)$ is equal to the lower-closed interval $(-\infty, \text{castAdd}\,m\,i]$ in $\text{Fin}(m + n)$. In symbols: $$\text{castAdd}\,m\big((-\infty, i]\big) = (-\infty, \text{castAdd}\,m\,i]$$

Fin.finsetImage_castAdd_Iio theorem

(m) (i : Fin n) : (Iio i).image (castAdd m) = Iio (castAdd m i)

Full source

@[simp]
theorem finsetImage_castAdd_Iio (m) (i : Fin n) : (Iio i).image (castAdd m) = Iio (castAdd m i) :=
  finsetImage_castLE_Iio ..

Image of Open Lower Interval under $\text{castAdd}\,m$ Equals Open Lower Interval of Image

Informal description

For any natural number $m$ and any element $i \in \text{Fin}(n)$, the image of the open lower interval $(-\infty, i)$ under the function $\text{castAdd}\,m : \text{Fin}(n) \to \text{Fin}(m + n)$ is equal to the open lower interval $(-\infty, \text{castAdd}\,m\,i)$ in $\text{Fin}(m + n)$. In symbols: $$\text{castAdd}\,m\big((-\infty, i)\big) = (-\infty, \text{castAdd}\,m\,i)$$

Fin.map_castAddEmb_Icc theorem

(m) (i j : Fin n) : (Icc i j).map (castAddEmb m) = Icc (castAddEmb m i) (castAddEmb m j)

Full source

@[simp]
theorem map_castAddEmb_Icc (m) (i j : Fin n) :
    (Icc i j).map (castAddEmb m) = Icc (castAddEmb m i) (castAddEmb m j) :=
  map_castLEEmb_Icc ..

Image of Closed Interval under $\text{castAddEmb}$ Equals Closed Interval in Target

Informal description

For any natural number $m$ and elements $i, j \in \text{Fin}(n)$, the image of the closed interval $[i, j]$ under the embedding $\text{castAddEmb}\,m : \text{Fin}(n) \to \text{Fin}(n + m)$ is equal to the closed interval $[\text{castAddEmb}\,m\,i, \text{castAddEmb}\,m\,j]$ in $\text{Fin}(n + m)$.

Fin.map_castAddEmb_Ico theorem

(m) (i j : Fin n) : (Ico i j).map (castAddEmb m) = Ico (castAddEmb m i) (castAddEmb m j)

Full source

@[simp]
theorem map_castAddEmb_Ico (m) (i j : Fin n) :
    (Ico i j).map (castAddEmb m) = Ico (castAddEmb m i) (castAddEmb m j) :=
  map_castLEEmb_Ico ..

Image of $[i, j)$ under $\text{castAddEmb}\,m$ equals $[\text{castAddEmb}\,m\,i, \text{castAddEmb}\,m\,j)$ in $\text{Fin}(n + m)$

Informal description

For any natural number $m$ and elements $i, j \in \text{Fin}(n)$, the image of the closed-open interval $[i, j)$ under the embedding $\text{castAddEmb}\,m : \text{Fin}(n) \to \text{Fin}(n + m)$ is equal to the closed-open interval $[\text{castAddEmb}\,m\,i, \text{castAddEmb}\,m\,j)$ in $\text{Fin}(n + m)$.

Fin.map_castAddEmb_Ioc theorem

(m) (i j : Fin n) : (Ioc i j).map (castAddEmb m) = Ioc (castAddEmb m i) (castAddEmb m j)

Full source

@[simp]
theorem map_castAddEmb_Ioc (m) (i j : Fin n) :
    (Ioc i j).map (castAddEmb m) = Ioc (castAddEmb m i) (castAddEmb m j) :=
  map_castLEEmb_Ioc ..

Image of Open-Closed Interval under $\text{castAddEmb}$ Equals Open-Closed Interval in Extended Type

Informal description

For any natural number $m$ and elements $i, j \in \text{Fin}(n)$, the image of the open-closed interval $(i, j]$ under the embedding $\text{castAddEmb}\,m$ is equal to the open-closed interval $(\text{castAddEmb}\,m\,i, \text{castAddEmb}\,m\,j]$ in $\text{Fin}(n + m)$.

Fin.map_castAddEmb_Ioo theorem

(m) (i j : Fin n) : (Ioo i j).map (castAddEmb m) = Ioo (castAddEmb m i) (castAddEmb m j)

Full source

@[simp]
theorem map_castAddEmb_Ioo (m) (i j : Fin n) :
    (Ioo i j).map (castAddEmb m) = Ioo (castAddEmb m i) (castAddEmb m j) :=
  map_castLEEmb_Ioo ..

Preservation of Open Interval under $\text{castAddEmb}$ Embedding

Informal description

For any natural number $m$ and elements $i, j \in \text{Fin}(n)$, the image of the open interval $(i, j)$ under the embedding $\text{castAddEmb}\,m$ is equal to the open interval $(\text{castAddEmb}\,m\,i, \text{castAddEmb}\,m\,j)$ in $\text{Fin}(n + m)$.

Fin.map_castAddEmb_uIcc theorem

(m) (i j : Fin n) : (uIcc i j).map (castAddEmb m) = uIcc (castAddEmb m i) (castAddEmb m j)

Full source

@[simp]
theorem map_castAddEmb_uIcc (m) (i j : Fin n) :
    (uIcc i j).map (castAddEmb m) = uIcc (castAddEmb m i) (castAddEmb m j) :=
  map_castLEEmb_uIcc ..

Preservation of Unordered Closed Interval under $\text{castAddEmb}$ Embedding

Informal description

For any natural number $m$ and elements $i, j \in \text{Fin}(n)$, the image of the unordered closed interval $\text{uIcc}(i, j)$ under the embedding $\text{castAddEmb}\,m$ is equal to the unordered closed interval $\text{uIcc}(\text{castAddEmb}\,m\,i, \text{castAddEmb}\,m\,j)$ in $\text{Fin}(n + m)$. In symbols: $$\text{castAddEmb}\,m\big(\text{uIcc}(i, j)\big) = \text{uIcc}(\text{castAddEmb}\,m\,i, \text{castAddEmb}\,m\,j)$$

Fin.map_castAddEmb_Ici theorem

(m) [NeZero m] (i : Fin n) : (Ici i).map (castAddEmb m) = Ico (castAddEmb m i) (natAdd n 0)

Full source

@[simp]
theorem map_castAddEmb_Ici (m) [NeZero m] (i : Fin n) :
    (Ici i).map (castAddEmb m) = Ico (castAddEmb m i) (natAdd n 0) := by
  simp [map_eq_image]

Image of $[i, \infty)$ under $\text{castAddEmb}\,m$ equals $[\text{castAddEmb}\,m\,i, \text{natAdd}\,n\,0)$ in $\text{Fin}\,(m + n)$

Informal description

For any natural number $m \neq 0$ and any element $i \in \text{Fin}\,n$, the image of the left-closed right-infinite interval $[i, \infty)$ under the embedding $\text{castAddEmb}\,m$ is equal to the left-closed right-open interval $[\text{castAddEmb}\,m\,i, \text{natAdd}\,n\,0)$ in $\text{Fin}\,(m + n)$. In symbols: $$ \text{castAddEmb}\,m([i, \infty)) = [\text{castAddEmb}\,m\,i, \text{natAdd}\,n\,0) $$

Fin.map_castAddEmb_Ioi theorem

(m) [NeZero m] (i : Fin n) : (Ioi i).map (castAddEmb m) = Ioo (castAddEmb m i) (natAdd n 0)

Full source

@[simp]
theorem map_castAddEmb_Ioi (m) [NeZero m] (i : Fin n) :
    (Ioi i).map (castAddEmb m) = Ioo (castAddEmb m i) (natAdd n 0) := by
  simp [← coe_inj]

Image of Right-Infinite Interval under $\text{castAddEmb}\,m$ Equals Open Interval

Informal description

For any natural number $m \neq 0$ and any element $i$ of $\text{Fin}\,n$, the image of the left-open right-infinite interval $(i, \infty)$ under the embedding $\text{castAddEmb}\,m$ is equal to the open interval $(\text{castAddEmb}\,m\,i, \text{natAdd}\,n\,0)$ in $\text{Fin}\,(m + n)$.

Fin.map_castAddEmb_Iic theorem

(m) (i : Fin n) : (Iic i).map (castAddEmb m) = Iic (castAddEmb m i)

Full source

@[simp]
theorem map_castAddEmb_Iic (m) (i : Fin n) : (Iic i).map (castAddEmb m) = Iic (castAddEmb m i) :=
  map_castLEEmb_Iic i _

Image of Lower-Closed Interval under $\text{castAddEmb}\,m$ Equals Lower-Closed Interval of Image

Informal description

For any natural number $m$ and any element $i \in \text{Fin}(n)$, the image of the lower-closed interval $(-\infty, i]$ under the embedding $\text{castAddEmb}\,m : \text{Fin}(n) \to \text{Fin}(m + n)$ is equal to the lower-closed interval $(-\infty, \text{castAddEmb}\,m\,i]$ in $\text{Fin}(m + n)$. In symbols: $$\text{castAddEmb}\,m\big((-\infty, i]\big) = (-\infty, \text{castAddEmb}\,m\,i]$$

Fin.map_castAddEmb_Iio theorem

(m) (i : Fin n) : (Iio i).map (castAddEmb m) = Iio (castAddEmb m i)

Full source

@[simp]
theorem map_castAddEmb_Iio (m) (i : Fin n) : (Iio i).map (castAddEmb m) = Iio (castAddEmb m i) :=
  map_castLEEmb_Iio ..

Image of Open Lower Interval under $\text{castAddEmb}$ Equals Open Lower Interval of Image

Informal description

For any natural number $m$ and any element $i \in \text{Fin}(n)$, the image of the open lower interval $(-\infty, i)$ under the embedding $\text{castAddEmb}\,m : \text{Fin}(n) \to \text{Fin}(m + n)$ is equal to the open lower interval $(-\infty, \text{castAddEmb}\,m\,i)$ in $\text{Fin}(m + n)$. In symbols: $$\text{castAddEmb}\,m\big((-\infty, i)\big) = (-\infty, \text{castAddEmb}\,m\,i)$$

Fin.finsetImage_cast_Icc theorem

(h : n = m) (i j : Fin n) : (Icc i j).image (.cast h) = Icc (i.cast h) (j.cast h)

Full source

@[simp]
theorem finsetImage_cast_Icc (h : n = m) (i j : Fin n) :
    (Icc i j).image (.cast h) = Icc (i.cast h) (j.cast h) := by
  simp [← coe_inj]

Image of Closed Interval under Fin Casting Function

Informal description

For natural numbers $n$ and $m$ with $n = m$, and for any elements $i, j \in \text{Fin}(n)$, the image of the closed interval $[i, j]$ under the cast function $\text{Fin.cast}\ h : \text{Fin}(n) \to \text{Fin}(m)$ is equal to the closed interval $[\text{Fin.cast}\ h\ i, \text{Fin.cast}\ h\ j]$ in $\text{Fin}(m)$. In other words: \[ \text{image}(\text{Fin.cast}\ h, [i, j]) = [\text{Fin.cast}\ h\ i, \text{Fin.cast}\ h\ j] \]

Fin.finsetImage_cast_Ico theorem

(h : n = m) (i j : Fin n) : (Ico i j).image (.cast h) = Ico (i.cast h) (j.cast h)

Full source

@[simp]
theorem finsetImage_cast_Ico (h : n = m) (i j : Fin n) :
    (Ico i j).image (.cast h) = Ico (i.cast h) (j.cast h) := by
  simp [← coe_inj]

Image of Closed-Open Interval under Fin Casting Function

Informal description

For natural numbers $n$ and $m$ with $n = m$, and for any elements $i, j \in \text{Fin}(n)$, the image of the closed-open interval $[i, j)$ under the cast function $\text{Fin.cast}\ h : \text{Fin}(n) \to \text{Fin}(m)$ is equal to the closed-open interval $[\text{Fin.cast}\ h\ i, \text{Fin.cast}\ h\ j)$ in $\text{Fin}(m)$. In other words: \[ \text{image}(\text{Fin.cast}\ h, [i, j)) = [\text{Fin.cast}\ h\ i, \text{Fin.cast}\ h\ j) \]

Fin.finsetImage_cast_Ioc theorem

(h : n = m) (i j : Fin n) : (Ioc i j).image (.cast h) = Ioc (i.cast h) (j.cast h)

Full source

@[simp]
theorem finsetImage_cast_Ioc (h : n = m) (i j : Fin n) :
    (Ioc i j).image (.cast h) = Ioc (i.cast h) (j.cast h) := by
  simp [← coe_inj]

Image of Open-Closed Interval under Fin Casting Function

Informal description

For any natural numbers $n$ and $m$ with $n = m$, and for any elements $i, j \in \text{Fin}(n)$, the image of the open-closed interval $[i, j)$ under the cast function $\text{Fin.cast}\ h : \text{Fin}(n) \to \text{Fin}(m)$ is equal to the open-closed interval $[i.\text{cast}\ h, j.\text{cast}\ h)$ in $\text{Fin}(m)$. In other words: \[ \text{image}(\text{Fin.cast}\ h, \text{Ioc}(i, j)) = \text{Ioc}(i.\text{cast}\ h, j.\text{cast}\ h) \]

Fin.finsetImage_cast_Ioo theorem

(h : n = m) (i j : Fin n) : (Ioo i j).image (.cast h) = Ioo (i.cast h) (j.cast h)

Full source

@[simp]
theorem finsetImage_cast_Ioo (h : n = m) (i j : Fin n) :
    (Ioo i j).image (.cast h) = Ioo (i.cast h) (j.cast h) := by
  simp [← coe_inj]

Image of Open Interval under Fin Casting Function

Informal description

For natural numbers $n$ and $m$ with $n = m$, and for any elements $i, j \in \text{Fin}(n)$, the image of the open interval finset $\text{Ioo}(i, j)$ under the cast function $\text{Fin.cast}\ h : \text{Fin}(n) \to \text{Fin}(m)$ is equal to the open interval finset $\text{Ioo}(i.\text{cast}\ h, j.\text{cast}\ h)$ in $\text{Fin}(m)$. In other words: \[ \text{image}(\text{Fin.cast}\ h, \text{Ioo}(i, j)) = \text{Ioo}(i.\text{cast}\ h, j.\text{cast}\ h) \]

Fin.finsetImage_cast_uIcc theorem

(h : n = m) (i j : Fin n) : (uIcc i j).image (.cast h) = uIcc (i.cast h) (j.cast h)

Full source

@[simp]
theorem finsetImage_cast_uIcc (h : n = m) (i j : Fin n) :
    (uIcc i j).image (.cast h) = uIcc (i.cast h) (j.cast h) := by
  simp [← coe_inj]

Image of Unordered Closed Interval under Fin Casting Function

Informal description

For any natural numbers $n$ and $m$ such that $n = m$, and for any elements $i, j \in \text{Fin}(n)$, the image of the unordered closed interval $\text{uIcc}(i, j)$ under the cast function $\text{Fin.cast}\ h : \text{Fin}(n) \to \text{Fin}(m)$ is equal to the unordered closed interval $\text{uIcc}(i.\text{cast}\ h, j.\text{cast}\ h)$ in $\text{Fin}(m)$. In other words: \[ \text{image}(\text{Fin.cast}\ h, \text{uIcc}(i, j)) = \text{uIcc}(i.\text{cast}\ h, j.\text{cast}\ h) \]

Fin.finsetImage_cast_Ici theorem

(h : n = m) (i : Fin n) : (Ici i).image (.cast h) = Ici (i.cast h)

Full source

@[simp]
theorem finsetImage_cast_Ici (h : n = m) (i : Fin n) :
    (Ici i).image (.cast h) = Ici (i.cast h) := by
  simp [← coe_inj]

Image of Closed-Infinite Interval under Fin Casting Function

Informal description

For any natural numbers $n$ and $m$ such that $n = m$, and for any element $i \in \text{Fin}(n)$, the image of the closed-infinite interval $\text{Ici}(i)$ under the cast function $\text{Fin.cast}\ h : \text{Fin}(n) \to \text{Fin}(m)$ is equal to the closed-infinite interval $\text{Ici}(i.\text{cast}\ h)$ in $\text{Fin}(m)$. In other words: \[ \text{image}(\text{Fin.cast}\ h)(\text{Ici}(i)) = \text{Ici}(i.\text{cast}\ h) \]

Fin.finsetImage_cast_Ioi theorem

(h : n = m) (i : Fin n) : (Ioi i).image (.cast h) = Ioi (i.cast h)

Full source

@[simp]
theorem finsetImage_cast_Ioi (h : n = m) (i : Fin n) :
    (Ioi i).image (.cast h) = Ioi (i.cast h) := by
  simp [← coe_inj]

Image of Open-Infinite Interval under Fin Casting Function

Informal description

For any natural numbers $n$ and $m$ such that $n = m$, and for any element $i \in \text{Fin}(n)$, the image of the open-infinite interval $(i, \infty)$ under the casting function $\text{Fin.cast}\ h : \text{Fin}(n) \to \text{Fin}(m)$ is equal to the open-infinite interval $(\text{Fin.cast}\ h\ i, \infty)$ in $\text{Fin}(m)$. In other words: \[ \text{image}(\text{Fin.cast}\ h, \text{Ioi}(i)) = \text{Ioi}(\text{Fin.cast}\ h\ i) \]

Fin.finsetImage_cast_Iic theorem

(h : n = m) (i : Fin n) : (Iic i).image (.cast h) = Iic (i.cast h)

Full source

@[simp]
theorem finsetImage_cast_Iic (h : n = m) (i : Fin n) :
    (Iic i).image (.cast h) = Iic (i.cast h) := by
  simp [← coe_inj]

Image of Lower-Closed Interval under Fin Casting: $\text{image}(\text{cast}, \text{Iic}(i)) = \text{Iic}(\text{cast}\ i)$

Informal description

For any natural numbers $n$ and $m$ such that $n = m$, and for any element $i \in \text{Fin}(n)$, the image of the lower-closed interval $\text{Iic}(i)$ under the cast function $\text{Fin.cast}\ h : \text{Fin}(n) \to \text{Fin}(m)$ is equal to the lower-closed interval $\text{Iic}(i.\text{cast}\ h)$ in $\text{Fin}(m)$. In other words: \[ \text{image}(\text{Fin.cast}\ h, \text{Iic}(i)) = \text{Iic}(i.\text{cast}\ h) \]

Fin.finsetImage_cast_Iio theorem

(h : n = m) (i : Fin n) : (Iio i).image (.cast h) = Iio (i.cast h)

Full source

@[simp]
theorem finsetImage_cast_Iio (h : n = m) (i : Fin n) :
    (Iio i).image (.cast h) = Iio (i.cast h) := by
  simp [← coe_inj]

Preservation of Open Lower Interval under Fin Casting

Informal description

For natural numbers $n$ and $m$ with $n = m$, and for any element $i \in \text{Fin}(n)$, the image of the open lower interval $\text{Iio}(i)$ under the casting function $\text{Fin.cast}\ h : \text{Fin}(n) \to \text{Fin}(m)$ is equal to the open lower interval $\text{Iio}(i.\text{cast}\ h)$ in $\text{Fin}(m)$. In other words: \[ \text{image}(\text{Fin.cast}\ h)(\{x \in \text{Fin}(n) \mid x < i\}) = \{y \in \text{Fin}(m) \mid y < i.\text{cast}\ h\} \]

Fin.map_finCongr_Icc theorem

(h : n = m) (i j : Fin n) : (Icc i j).map (finCongr h).toEmbedding = Icc (i.cast h) (j.cast h)

Full source

@[simp]
theorem map_finCongr_Icc (h : n = m) (i j : Fin n) :
    (Icc i j).map (finCongr h).toEmbedding = Icc (i.cast h) (j.cast h) := by
  simp [← coe_inj]

Preservation of Closed Intervals under Order Isomorphism in $\text{Fin}(n)$

Informal description

For any natural numbers $n$ and $m$ such that $n = m$, and for any elements $i, j \in \text{Fin}(n)$, the image of the closed interval $[i, j]$ under the order isomorphism $\text{finCongr}\ h : \text{Fin}(n) \to \text{Fin}(m)$ is equal to the closed interval $[i.\text{cast}\ h, j.\text{cast}\ h]$ in $\text{Fin}(m)$. In other words, the map preserves the closed interval structure: \[ \text{map}(\text{finCongr}\ h) ([i, j]) = [i.\text{cast}\ h, j.\text{cast}\ h] \]

Fin.map_finCongr_Ico theorem

(h : n = m) (i j : Fin n) : (Ico i j).map (finCongr h).toEmbedding = Ico (i.cast h) (j.cast h)

Full source

@[simp]
theorem map_finCongr_Ico (h : n = m) (i j : Fin n) :
    (Ico i j).map (finCongr h).toEmbedding = Ico (i.cast h) (j.cast h) := by
  simp [← coe_inj]

Preservation of Closed-Open Intervals under Fin Order Isomorphism

Informal description

For any natural numbers $n$ and $m$ such that $n = m$, and for any elements $i, j \in \text{Fin}(n)$, the image of the closed-open interval $[i, j)$ under the order isomorphism $\text{finCongr}\ h : \text{Fin}(n) \to \text{Fin}(m)$ is equal to the closed-open interval $[i.\text{cast}\ h, j.\text{cast}\ h)$ in $\text{Fin}(m)$. In other words: \[ \text{map}(\text{finCongr}\ h.\text{toEmbedding})([i, j)) = [i.\text{cast}\ h, j.\text{cast}\ h) \]

Fin.map_finCongr_Ioc theorem

(h : n = m) (i j : Fin n) : (Ioc i j).map (finCongr h).toEmbedding = Ioc (i.cast h) (j.cast h)

Full source

@[simp]
theorem map_finCongr_Ioc (h : n = m) (i j : Fin n) :
    (Ioc i j).map (finCongr h).toEmbedding = Ioc (i.cast h) (j.cast h) := by
  simp [← coe_inj]

Preservation of Open-Closed Intervals under Fin Order Isomorphism

Informal description

For any natural numbers $n$ and $m$ such that $n = m$, and for any elements $i, j \in \text{Fin}(n)$, the image of the open-closed interval $\text{Ioc}(i, j)$ under the order isomorphism $\text{finCongr}\ h$ is equal to the open-closed interval $\text{Ioc}(i.\text{cast}\ h, j.\text{cast}\ h)$ in $\text{Fin}(m)$. In other words: \[ \text{finCongr}\ h[\text{Ioc}(i, j)] = \text{Ioc}(i.\text{cast}\ h, j.\text{cast}\ h) \] where $\text{finCongr}\ h$ is the order isomorphism between $\text{Fin}(n)$ and $\text{Fin}(m)$ induced by the equality $h : n = m$, and $i.\text{cast}\ h$ denotes the casting of $i$ from $\text{Fin}(n)$ to $\text{Fin}(m)$ via $h$.

Fin.map_finCongr_Ioo theorem

(h : n = m) (i j : Fin n) : (Ioo i j).map (finCongr h).toEmbedding = Ioo (i.cast h) (j.cast h)

Full source

@[simp]
theorem map_finCongr_Ioo (h : n = m) (i j : Fin n) :
    (Ioo i j).map (finCongr h).toEmbedding = Ioo (i.cast h) (j.cast h) := by
  simp [← coe_inj]

Preservation of Open Intervals under Fin Type Isomorphism

Informal description

For natural numbers $n$ and $m$ with $n = m$, and for any elements $i, j \in \text{Fin}(n)$, the image of the open interval $\text{Ioo}(i, j)$ under the embedding $\text{finCongr}\ h$ is equal to the open interval $\text{Ioo}(i.\text{cast}\ h, j.\text{cast}\ h)$ in $\text{Fin}(m)$. In other words, the following equality holds: \[ \text{map}\ (\text{finCongr}\ h).\text{toEmbedding}\ (\text{Ioo}\ i\ j) = \text{Ioo}\ (i.\text{cast}\ h)\ (j.\text{cast}\ h) \]

Fin.map_finCongr_uIcc theorem

(h : n = m) (i j : Fin n) : (uIcc i j).map (finCongr h).toEmbedding = uIcc (i.cast h) (j.cast h)

Full source

@[simp]
theorem map_finCongr_uIcc (h : n = m) (i j : Fin n) :
    (uIcc i j).map (finCongr h).toEmbedding = uIcc (i.cast h) (j.cast h) := by
  simp [← coe_inj]

Preservation of Unordered Closed Intervals under Fin Order Isomorphism

Informal description

For natural numbers $n$ and $m$ with $n = m$, and for any elements $i, j \in \text{Fin}(n)$, the image of the unordered closed interval $\text{uIcc}(i, j)$ under the order isomorphism $\text{finCongr}\ h : \text{Fin}(n) \to \text{Fin}(m)$ is equal to the unordered closed interval $\text{uIcc}(i.\text{cast}\ h, j.\text{cast}\ h)$ in $\text{Fin}(m)$. In other words: \[ (\text{uIcc}\ i\ j).\text{map}\ (\text{finCongr}\ h).\text{toEmbedding} = \text{uIcc}\ (i.\text{cast}\ h)\ (j.\text{cast}\ h) \]

Fin.map_finCongr_Ici theorem

(h : n = m) (i : Fin n) : (Ici i).map (finCongr h).toEmbedding = Ici (i.cast h)

Full source

@[simp]
theorem map_finCongr_Ici (h : n = m) (i : Fin n) :
    (Ici i).map (finCongr h).toEmbedding = Ici (i.cast h) := by
  simp [← coe_inj]

Preservation of Closed Right-Infinite Interval under Fin Order Isomorphism

Informal description

For natural numbers $n$ and $m$ with $n = m$, and for any $i \in \text{Fin}(n)$, the image of the closed right-infinite interval $[i, \infty)$ under the order isomorphism $\text{finCongr}\ h : \text{Fin}(n) \to \text{Fin}(m)$ is equal to the closed right-infinite interval $[i.\text{cast}\ h, \infty)$ in $\text{Fin}(m)$. In other words: \[ (\text{Ici}\ i).\text{map}\ (\text{finCongr}\ h).\text{toEmbedding} = \text{Ici}\ (i.\text{cast}\ h) \]

Fin.map_finCongr_Ioi theorem

(h : n = m) (i : Fin n) : (Ioi i).map (finCongr h).toEmbedding = Ioi (i.cast h)

Full source

@[simp]
theorem map_finCongr_Ioi (h : n = m) (i : Fin n) :
    (Ioi i).map (finCongr h).toEmbedding = Ioi (i.cast h) := by
  simp [← coe_inj]

Image of Open Right-Infinite Interval under Fin Order Isomorphism

Informal description

For natural numbers $n$ and $m$ with $n = m$, and for any $i \in \text{Fin}(n)$, the image of the open right-infinite interval $(i, \infty)$ under the order isomorphism $\text{finCongr}\ h : \text{Fin}(n) \to \text{Fin}(m)$ is equal to the open right-infinite interval $(i.\text{cast}\ h, \infty)$ in $\text{Fin}(m)$. In other words: \[ (\text{Ioi}\ i).\text{map}\ (\text{finCongr}\ h).\text{toEmbedding} = \text{Ioi}\ (i.\text{cast}\ h) \]

Fin.map_finCongr_Iic theorem

(h : n = m) (i : Fin n) : (Iic i).map (finCongr h).toEmbedding = Iic (i.cast h)

Full source

@[simp]
theorem map_finCongr_Iic (h : n = m) (i : Fin n) :
    (Iic i).map (finCongr h).toEmbedding = Iic (i.cast h) := by
  simp [← coe_inj]

Preservation of Lower-Closed Interval under Fin Order Isomorphism

Informal description

For any natural numbers $n$ and $m$ such that $n = m$, and for any element $i \in \text{Fin}(n)$, the image of the lower-closed interval $\text{Iic}(i)$ under the order isomorphism $\text{finCongr}\ h : \text{Fin}(n) \to \text{Fin}(m)$ is equal to the lower-closed interval $\text{Iic}(i.\text{cast}\ h)$ in $\text{Fin}(m)$. In other words: \[ (\text{Iic}\ i).\text{map}\ (\text{finCongr}\ h).\text{toEmbedding} = \text{Iic}\ (i.\text{cast}\ h) \]

Fin.map_finCongr_Iio theorem

(h : n = m) (i : Fin n) : (Iio i).map (finCongr h).toEmbedding = Iio (i.cast h)

Full source

@[simp]
theorem map_finCongr_Iio (h : n = m) (i : Fin n) :
    (Iio i).map (finCongr h).toEmbedding = Iio (i.cast h) := by
  simp [← coe_inj]

Preservation of Open Lower Interval under Fin Congruence Casting

Informal description

For natural numbers $n$ and $m$ with $h : n = m$, and for any $i \in \text{Fin}(n)$, the image of the open lower interval $\text{Iio}(i)$ under the embedding $\text{finCongr}\ h$ is equal to the open lower interval $\text{Iio}(i.\text{cast}\ h)$ in $\text{Fin}(m)$. In symbols: \[ \text{map}\ (\text{finCongr}\ h).\text{toEmbedding}\ (\text{Iio}\ i) = \text{Iio}\ (i.\text{cast}\ h) \]

Fin.finsetImage_castSucc_Icc theorem

(i j : Fin n) : (Icc i j).image castSucc = Icc i.castSucc j.castSucc

Full source

@[simp]
theorem finsetImage_castSucc_Icc (i j : Fin n) :
    (Icc i j).image castSucc = Icc i.castSucc j.castSucc :=
  finsetImage_castAdd_Icc ..

Image of Closed Interval under Successor Embedding in Finite Types

Informal description

For any elements $i, j \in \text{Fin}(n)$, the image of the closed interval $[i, j]$ under the successor embedding $\text{castSucc} : \text{Fin}(n) \to \text{Fin}(n+1)$ is equal to the closed interval $[\text{castSucc}\,i, \text{castSucc}\,j]$ in $\text{Fin}(n+1)$. In symbols: \[ \text{image}\ \text{castSucc}\ ([i, j]) = [\text{castSucc}\,i, \text{castSucc}\,j] \]

Fin.finsetImage_castSucc_Ico theorem

(i j : Fin n) : (Ico i j).image castSucc = Ico i.castSucc j.castSucc

Full source

@[simp]
theorem finsetImage_castSucc_Ico (i j : Fin n) :
    (Ico i j).image castSucc = Ico i.castSucc j.castSucc :=
  finsetImage_castAdd_Ico ..

Image of $[i, j)$ under $\text{castSucc}$ equals $[\text{castSucc}(i), \text{castSucc}(j))$ in $\text{Fin}(n+1)$

Informal description

For any elements $i, j \in \text{Fin}(n)$, the image of the closed-open interval $[i, j)$ under the successor embedding $\text{castSucc} : \text{Fin}(n) \to \text{Fin}(n+1)$ is equal to the closed-open interval $[\text{castSucc}(i), \text{castSucc}(j))$ in $\text{Fin}(n+1)$.

Fin.finsetImage_castSucc_Ioc theorem

(i j : Fin n) : (Ioc i j).image castSucc = Ioc i.castSucc j.castSucc

Full source

@[simp]
theorem finsetImage_castSucc_Ioc (i j : Fin n) :
    (Ioc i j).image castSucc = Ioc i.castSucc j.castSucc :=
  finsetImage_castAdd_Ioc ..

Image of $(i, j]$ under $\text{castSucc}$ equals $(\text{castSucc}(i), \text{castSucc}(j)]$ in $\text{Fin}(n+1)$

Informal description

For any elements $i, j \in \text{Fin}(n)$, the image of the left-open right-closed interval $(i, j]$ under the successor embedding $\text{castSucc} : \text{Fin}(n) \to \text{Fin}(n+1)$ is equal to the left-open right-closed interval $(\text{castSucc}(i), \text{castSucc}(j)]$ in $\text{Fin}(n+1)$. In symbols: \[ \text{image}\ \text{castSucc}\ ((i, j]) = (\text{castSucc}(i), \text{castSucc}(j)] \]

Fin.finsetImage_castSucc_Ioo theorem

(i j : Fin n) : (Ioo i j).image castSucc = Ioo i.castSucc j.castSucc

Full source

@[simp]
theorem finsetImage_castSucc_Ioo (i j : Fin n) :
    (Ioo i j).image castSucc = Ioo i.castSucc j.castSucc :=
  finsetImage_castAdd_Ioo ..

Image of Open Interval under Successor Embedding in Finite Types

Informal description

For any elements $i, j \in \text{Fin}(n)$, the image of the open interval $(i, j)$ under the successor embedding $\text{castSucc} : \text{Fin}(n) \to \text{Fin}(n+1)$ is equal to the open interval $(\text{castSucc}(i), \text{castSucc}(j))$ in $\text{Fin}(n+1)$.

Fin.finsetImage_castSucc_uIcc theorem

(i j : Fin n) : (uIcc i j).image castSucc = uIcc i.castSucc j.castSucc

Full source

@[simp]
theorem finsetImage_castSucc_uIcc (i j : Fin n) :
    (uIcc i j).image castSucc = uIcc i.castSucc j.castSucc :=
  finsetImage_castAdd_uIcc ..

Preservation of Unordered Closed Interval under Successor Embedding in Finite Types

Informal description

For any elements $i, j$ in $\text{Fin}(n)$, the image of the unordered closed interval $\text{uIcc}(i, j)$ under the successor embedding $\text{castSucc} : \text{Fin}(n) \to \text{Fin}(n+1)$ is equal to the unordered closed interval $\text{uIcc}(\text{castSucc}(i), \text{castSucc}(j))$ in $\text{Fin}(n+1)$. In symbols: \[ \text{castSucc}(\text{uIcc}(i, j)) = \text{uIcc}(\text{castSucc}(i), \text{castSucc}(j)) \]

Fin.finsetImage_castSucc_Ici theorem

(i : Fin n) : (Ici i).image castSucc = Ico i.castSucc (.last n)

Full source

@[simp]
theorem finsetImage_castSucc_Ici (i : Fin n) : (Ici i).image castSucc = Ico i.castSucc (.last n) :=
  finsetImage_castAdd_Ici ..

Image of $[i, \infty)$ under $\text{castSucc}$ equals $[\text{castSucc}\,i, \text{last}\,n)$ in $\text{Fin}\,(n+1)$

Informal description

For any element $i$ in $\text{Fin}\,n$, the image of the left-closed right-infinite interval $[i, \infty)$ under the successor embedding $\text{castSucc}$ is equal to the left-closed right-open interval $[\text{castSucc}\,i, \text{last}\,n)$ in $\text{Fin}\,(n+1)$. In symbols: $$ \text{castSucc}([i, \infty)) = [\text{castSucc}\,i, \text{last}\,n) $$

Fin.finsetImage_castSucc_Ioi theorem

(i : Fin n) : (Ioi i).image castSucc = Ioo i.castSucc (.last n)

Full source

@[simp]
theorem finsetImage_castSucc_Ioi (i : Fin n) : (Ioi i).image castSucc = Ioo i.castSucc (.last n) :=
  finsetImage_castAdd_Ioi ..

Image of Right-Infinite Interval under Successor Embedding Equals Open Interval

Informal description

For any element $i$ in $\text{Fin}\,n$, the image of the open right-infinite interval $(i, \infty)$ under the successor embedding $\text{castSucc}$ is equal to the open interval $(\text{castSucc}\,i, \text{last}\,n)$ in $\text{Fin}\,(n + 1)$. In symbols: $$ \text{castSucc}\big((i, \infty)\big) = \big(\text{castSucc}\,i, \text{last}\,n\big) $$

Fin.finsetImage_castSucc_Iic theorem

(i : Fin n) : (Iic i).image castSucc = Iic i.castSucc

Full source

@[simp]
theorem finsetImage_castSucc_Iic (i : Fin n) : (Iic i).image castSucc = Iic i.castSucc :=
  finsetImage_castAdd_Iic ..

Image of Lower-Closed Interval under Successor Embedding in Finite Types

Informal description

For any element $i \in \text{Fin}(n)$, the image of the lower-closed interval $(-\infty, i]$ under the successor embedding $\text{castSucc} : \text{Fin}(n) \to \text{Fin}(n+1)$ is equal to the lower-closed interval $(-\infty, \text{castSucc}\,i]$ in $\text{Fin}(n+1)$. In symbols: $$\text{castSucc}\big((-\infty, i]\big) = (-\infty, \text{castSucc}\,i]$$

Fin.finsetImage_castSucc_Iio theorem

(i : Fin n) : (Iio i).image castSucc = Iio i.castSucc

Full source

@[simp]
theorem finsetImage_castSucc_Iio (i : Fin n) : (Iio i).image castSucc = Iio i.castSucc :=
  finsetImage_castAdd_Iio ..

Image of Open Lower Interval under Successor Embedding Equals Open Lower Interval of Image

Informal description

For any element $i$ in $\text{Fin}\,n$, the image of the open lower interval $(-\infty, i)$ under the successor embedding $\text{castSucc} : \text{Fin}\,n \to \text{Fin}\,(n + 1)$ is equal to the open lower interval $(-\infty, \text{castSucc}\,i)$ in $\text{Fin}\,(n + 1)$. In symbols: $$ \text{castSucc}\big((-\infty, i)\big) = (-\infty, \text{castSucc}\,i) $$

Fin.map_castSuccEmb_Icc theorem

(i j : Fin n) : (Icc i j).map castSuccEmb = Icc i.castSucc j.castSucc

Full source

@[simp]
theorem map_castSuccEmb_Icc (i j : Fin n) :
    (Icc i j).map castSuccEmb = Icc i.castSucc j.castSucc :=
  map_castAddEmb_Icc ..

Image of Closed Interval under Successor Embedding in Finite Types

Informal description

For any elements $i, j$ in $\text{Fin}(n)$, the image of the closed interval $[i, j]$ under the embedding $\text{castSuccEmb} : \text{Fin}(n) \to \text{Fin}(n+1)$ is equal to the closed interval $[\text{castSuccEmb}(i), \text{castSuccEmb}(j)]$ in $\text{Fin}(n+1)$.

Fin.map_castSuccEmb_Ico theorem

(i j : Fin n) : (Ico i j).map castSuccEmb = Ico i.castSucc j.castSucc

Full source

@[simp]
theorem map_castSuccEmb_Ico (i j : Fin n) :
    (Ico i j).map castSuccEmb = Ico i.castSucc j.castSucc :=
  map_castAddEmb_Ico ..

Image of $[i, j)$ under $\text{castSuccEmb}$ equals $[\text{castSuccEmb}(i), \text{castSuccEmb}(j))$ in $\text{Fin}(n+1)$

Informal description

For any elements $i, j$ in $\text{Fin}(n)$, the image of the closed-open interval $[i, j)$ under the embedding $\text{castSuccEmb} : \text{Fin}(n) \to \text{Fin}(n+1)$ is equal to the closed-open interval $[\text{castSuccEmb}(i), \text{castSuccEmb}(j))$ in $\text{Fin}(n+1)$.

Fin.map_castSuccEmb_Ioc theorem

(i j : Fin n) : (Ioc i j).map castSuccEmb = Ioc i.castSucc j.castSucc

Full source

@[simp]
theorem map_castSuccEmb_Ioc (i j : Fin n) :
    (Ioc i j).map castSuccEmb = Ioc i.castSucc j.castSucc :=
  map_castAddEmb_Ioc ..

Image of Open-Closed Interval under $\text{castSuccEmb}$ Equals Open-Closed Interval in Successor Type

Informal description

For any elements $i, j$ in $\text{Fin}(n)$, the image of the open-closed interval $(i, j]$ under the embedding $\text{castSuccEmb}$ is equal to the open-closed interval $(i.\text{castSucc}, j.\text{castSucc}]$ in $\text{Fin}(n+1)$.

Fin.map_castSuccEmb_Ioo theorem

(i j : Fin n) : (Ioo i j).map castSuccEmb = Ioo i.castSucc j.castSucc

Full source

@[simp]
theorem map_castSuccEmb_Ioo (i j : Fin n) :
    (Ioo i j).map castSuccEmb = Ioo i.castSucc j.castSucc :=
  map_castAddEmb_Ioo ..

Preservation of Open Interval under Successor Embedding in Finite Types

Informal description

For any elements $i, j$ in $\text{Fin}(n)$, the image of the open interval $(i, j)$ under the embedding $\text{castSuccEmb}$ is equal to the open interval $(\text{castSuccEmb}\,i, \text{castSuccEmb}\,j)$ in $\text{Fin}(n+1)$.

Fin.map_castSuccEmb_uIcc theorem

(i j : Fin n) : (uIcc i j).map castSuccEmb = uIcc i.castSucc j.castSucc

Full source

@[simp]
theorem map_castSuccEmb_uIcc (i j : Fin n) :
    (uIcc i j).map castSuccEmb = uIcc i.castSucc j.castSucc :=
  map_castAddEmb_uIcc ..

Preservation of Unordered Closed Interval under Successor Embedding in Finite Types

Informal description

For any elements $i, j$ in $\text{Fin}(n)$, the image of the unordered closed interval $\text{uIcc}(i, j)$ under the successor embedding $\text{castSuccEmb}$ is equal to the unordered closed interval $\text{uIcc}(i.\text{castSucc}, j.\text{castSucc})$ in $\text{Fin}(n+1)$. In symbols: $$\text{castSuccEmb}(\text{uIcc}(i, j)) = \text{uIcc}(\text{castSuccEmb}\,i, \text{castSuccEmb}\,j)$$

Fin.map_castSuccEmb_Ici theorem

(i : Fin n) : (Ici i).map castSuccEmb = Ico i.castSucc (.last n)

Full source

@[simp]
theorem map_castSuccEmb_Ici (i : Fin n) : (Ici i).map castSuccEmb = Ico i.castSucc (.last n) :=
  map_castAddEmb_Ici ..

Image of Closed-Infinite Interval under Successor Embedding Equals Closed-Open Interval

Informal description

For any element $i$ in $\text{Fin}(n)$, the image of the left-closed right-infinite interval $[i, \infty)$ under the successor embedding $\text{castSuccEmb}$ is equal to the left-closed right-open interval $[i.\text{castSucc}, \text{last}\,n)$ in $\text{Fin}(n+1)$. In symbols: $$ \text{castSuccEmb}([i, \infty)) = [i.\text{castSucc}, \text{last}\,n) $$

Fin.map_castSuccEmb_Ioi theorem

(i : Fin n) : (Ioi i).map castSuccEmb = Ioo i.castSucc (.last n)

Full source

@[simp]
theorem map_castSuccEmb_Ioi (i : Fin n) : (Ioi i).map castSuccEmb = Ioo i.castSucc (.last n) :=
  map_castAddEmb_Ioi ..

Image of Right-Infinite Interval under Successor Embedding Equals Open Interval

Informal description

For any element $i$ in $\text{Fin}(n)$, the image of the right-infinite open interval $(i, \infty)$ under the embedding $\text{castSuccEmb}$ is equal to the open interval $(i.\text{castSucc}, \text{last}\,n)$ in $\text{Fin}(n+1)$.

Fin.map_castSuccEmb_Iic theorem

(i : Fin n) : (Iic i).map castSuccEmb = Iic i.castSucc

Full source

@[simp]
theorem map_castSuccEmb_Iic (i : Fin n) : (Iic i).map castSuccEmb = Iic i.castSucc :=
  map_castAddEmb_Iic ..

Preservation of Lower-Closed Interval under Successor Embedding in Finite Types

Informal description

For any element $i$ in the finite type $\text{Fin}(n)$, the image of the lower-closed interval $(-\infty, i]$ under the successor embedding $\text{castSuccEmb} : \text{Fin}(n) \to \text{Fin}(n+1)$ is equal to the lower-closed interval $(-\infty, \text{castSuccEmb}(i)]$ in $\text{Fin}(n+1)$. In symbols: $$\text{castSuccEmb}\big((-\infty, i]\big) = (-\infty, \text{castSuccEmb}(i)]$$

Fin.map_castSuccEmb_Iio theorem

(i : Fin n) : (Iio i).map castSuccEmb = Iio i.castSucc

Full source

@[simp]
theorem map_castSuccEmb_Iio (i : Fin n) : (Iio i).map castSuccEmb = Iio i.castSucc :=
  map_castAddEmb_Iio ..

Image of Open Lower Interval under Successor Embedding in $\text{Fin}(n)$

Informal description

For any element $i$ in $\text{Fin}(n)$, the image of the open lower interval $(-\infty, i)$ under the successor embedding $\text{castSuccEmb} : \text{Fin}(n) \to \text{Fin}(n+1)$ is equal to the open lower interval $(-\infty, \text{castSuccEmb}(i))$ in $\text{Fin}(n+1)$. In symbols: $$\text{castSuccEmb}\big((-\infty, i)\big) = (-\infty, \text{castSuccEmb}(i))$$

Fin.finsetImage_natAdd_Icc theorem

(m) (i j : Fin n) : (Icc i j).image (natAdd m) = Icc (natAdd m i) (natAdd m j)

Full source

@[simp]
theorem finsetImage_natAdd_Icc (m) (i j : Fin n) :
    (Icc i j).image (natAdd m) = Icc (natAdd m i) (natAdd m j) := by
  simp [← coe_inj]

Image of Closed Interval under `natAdd` in Finite Types

Informal description

For any natural number $m$ and any elements $i, j$ in $\text{Fin}\ n$, the image of the closed interval $[i, j]$ under the function $\text{natAdd}\ m : \text{Fin}\ n \to \text{Fin}\ (m + n)$ is equal to the closed interval $[\text{natAdd}\ m\ i, \text{natAdd}\ m\ j]$. In other words: $$(\text{Icc}(i, j)).\text{image}(\text{natAdd}\ m) = \text{Icc}(\text{natAdd}\ m\ i, \text{natAdd}\ m\ j)$$

Fin.finsetImage_natAdd_Ico theorem

(m) (i j : Fin n) : (Ico i j).image (natAdd m) = Ico (natAdd m i) (natAdd m j)

Full source

@[simp]
theorem finsetImage_natAdd_Ico (m) (i j : Fin n) :
    (Ico i j).image (natAdd m) = Ico (natAdd m i) (natAdd m j) := by
  simp [← coe_inj]

Image of Closed-Open Interval under `natAdd` in Finite Types

Informal description

For any natural number $m$ and any elements $i, j$ in $\text{Fin}\ n$, the image of the left-closed right-open interval $[i, j)$ under the function $\text{natAdd}\ m : \text{Fin}\ n \to \text{Fin}\ (m + n)$ is equal to the left-closed right-open interval $[\text{natAdd}\ m\ i, \text{natAdd}\ m\ j)$. In other words: $$(\text{natAdd}\ m)([i, j)) = [\text{natAdd}\ m\ i, \text{natAdd}\ m\ j)$$

Fin.finsetImage_natAdd_Ioc theorem

(m) (i j : Fin n) : (Ioc i j).image (natAdd m) = Ioc (natAdd m i) (natAdd m j)

Full source

@[simp]
theorem finsetImage_natAdd_Ioc (m) (i j : Fin n) :
    (Ioc i j).image (natAdd m) = Ioc (natAdd m i) (natAdd m j) := by
  simp [← coe_inj]

Image of $(i, j]$ under $\text{natAdd}\ m$ equals $(\text{natAdd}\ m\ i, \text{natAdd}\ m\ j]$ in $\text{Fin}\ n$

Informal description

For any natural number $m$ and elements $i, j$ in $\text{Fin}\ n$, the image of the left-open right-closed interval $(i, j]$ under the function $\text{natAdd}\ m$ is equal to the left-open right-closed interval $(\text{natAdd}\ m\ i, \text{natAdd}\ m\ j]$. In other words: $$(\text{natAdd}\ m) \big((i, j]\big) = (\text{natAdd}\ m\ i, \text{natAdd}\ m\ j]$$ where $(i, j]$ denotes the finset $\text{Ioc}(i, j)$.

Fin.finsetImage_natAdd_Ioo theorem

(m) (i j : Fin n) : (Ioo i j).image (natAdd m) = Ioo (natAdd m i) (natAdd m j)

Full source

@[simp]
theorem finsetImage_natAdd_Ioo (m) (i j : Fin n) :
    (Ioo i j).image (natAdd m) = Ioo (natAdd m i) (natAdd m j) := by
  simp [← coe_inj]

Image of Open Interval Finset under $\text{natAdd}(m)$ in Finite Types

Informal description

For any natural number $m$ and any elements $i, j$ in $\text{Fin}\ n$, the image of the open interval finset $(i, j)$ under the function $\text{natAdd}\ m : \text{Fin}\ n \to \text{Fin}\ (m + n)$ is equal to the open interval finset $(\text{natAdd}\ m\ i, \text{natAdd}\ m\ j)$. In other words: $$(\text{natAdd}\ m)((i, j)) = (\text{natAdd}\ m\ i, \text{natAdd}\ m\ j)$$

Fin.finsetImage_natAdd_uIcc theorem

(m) (i j : Fin n) : (uIcc i j).image (natAdd m) = uIcc (natAdd m i) (natAdd m j)

Full source

@[simp]
theorem finsetImage_natAdd_uIcc (m) (i j : Fin n) :
    (uIcc i j).image (natAdd m) = uIcc (natAdd m i) (natAdd m j) := by
  simp [← coe_inj]

Image of Unordered Closed Interval under `natAdd` in Finite Types

Informal description

For any natural number $m$ and any elements $i, j$ in $\text{Fin}\ n$, the image of the unordered closed interval finset $\text{uIcc}(i, j)$ under the function $\text{natAdd}\ m : \text{Fin}\ n \to \text{Fin}\ (m + n)$ is equal to the unordered closed interval finset $\text{uIcc}(\text{natAdd}\ m\ i, \text{natAdd}\ m\ j)$. In other words: $$(\text{natAdd}\ m)(\text{uIcc}(i, j)) = \text{uIcc}(\text{natAdd}\ m\ i, \text{natAdd}\ m\ j)$$

Fin.finsetImage_natAdd_Ici theorem

(m) (i : Fin n) : (Ici i).image (natAdd m) = Ici (natAdd m i)

Full source

@[simp]
theorem finsetImage_natAdd_Ici (m) (i : Fin n) : (Ici i).image (natAdd m) = Ici (natAdd m i) := by
  simp [← coe_inj]

Image of Left-Closed Interval Finset under $\text{natAdd}(m)$ in Finite Types

Informal description

For any natural number $m$ and any element $i$ in $\text{Fin}\ n$, the image of the left-closed right-infinite interval finset $[i, \infty)$ under the function $\text{natAdd}\ m : \text{Fin}\ n \to \text{Fin}\ (m + n)$ is equal to the left-closed right-infinite interval finset $[\text{natAdd}\ m\ i, \infty)$. In other words: $$(\text{natAdd}\ m)([i, \infty)) = [\text{natAdd}\ m\ i, \infty)$$

Fin.finsetImage_natAdd_Ioi theorem

(m) (i : Fin n) : (Ioi i).image (natAdd m) = Ioi (natAdd m i)

Full source

@[simp]
theorem finsetImage_natAdd_Ioi (m) (i : Fin n) : (Ioi i).image (natAdd m) = Ioi (natAdd m i) := by
  simp [← coe_inj]

Image of Open Infinite Interval under `natAdd` in Finite Types

Informal description

For any natural number $m$ and any element $i$ in $\text{Fin}\ n$, the image of the finset $(i, \infty)$ under the function $\text{natAdd}\ m : \text{Fin}\ n \to \text{Fin}\ (m + n)$ is equal to the finset $(\text{natAdd}\ m\ i, \infty)$. In other words: $$(\text{natAdd}\ m) \big( (i, \infty) \big) = (\text{natAdd}\ m\ i, \infty)$$

Fin.map_natAddEmb_Icc theorem

(m) (i j : Fin n) : (Icc i j).map (natAddEmb m) = Icc (natAdd m i) (natAdd m j)

Full source

@[simp]
theorem map_natAddEmb_Icc (m) (i j : Fin n) :
    (Icc i j).map (natAddEmb m) = Icc (natAdd m i) (natAdd m j) := by
  simp [← coe_inj]

Image of Closed Interval under `natAddEmb` in Finite Types

Informal description

For any natural number $m$ and elements $i, j$ in $\text{Fin}\ n$, the image of the closed interval $[i, j]$ under the embedding $\text{natAddEmb}\ m$ is equal to the closed interval $[\text{natAdd}\ m\ i, \text{natAdd}\ m\ j]$. In other words: $$(\text{natAddEmb}\ m)([i, j]) = [\text{natAdd}\ m\ i, \text{natAdd}\ m\ j]$$

Fin.map_natAddEmb_Ico theorem

(m) (i j : Fin n) : (Ico i j).map (natAddEmb m) = Ico (natAdd m i) (natAdd m j)

Full source

@[simp]
theorem map_natAddEmb_Ico (m) (i j : Fin n) :
    (Ico i j).map (natAddEmb m) = Ico (natAdd m i) (natAdd m j) := by
  simp [← coe_inj]

Image of Interval $[i, j)$ under $\text{natAddEmb}\ m$ in $\text{Fin}\ n$

Informal description

For any natural number $m$ and elements $i, j$ in $\text{Fin}\ n$, the image of the left-closed right-open interval $[i, j)$ under the embedding $\text{natAddEmb}\ m$ is equal to the left-closed right-open interval $[\text{natAdd}\ m\ i, \text{natAdd}\ m\ j)$. In other words: $$\text{natAddEmb}\ m([i, j)) = [\text{natAdd}\ m\ i, \text{natAdd}\ m\ j)$$

Fin.map_natAddEmb_Ioc theorem

(m) (i j : Fin n) : (Ioc i j).map (natAddEmb m) = Ioc (natAdd m i) (natAdd m j)

Full source

@[simp]
theorem map_natAddEmb_Ioc (m) (i j : Fin n) :
    (Ioc i j).map (natAddEmb m) = Ioc (natAdd m i) (natAdd m j) := by
  simp [← coe_inj]

Image of Left-Open Right-Closed Interval under `natAddEmb` in Finite Types

Informal description

For any natural number $m$ and any elements $i, j$ in $\text{Fin}\ n$, the image of the left-open right-closed interval $(i, j]$ under the embedding $\text{natAddEmb}\ m : \text{Fin}\ n \to \text{Fin}\ (m + n)$ is equal to the left-open right-closed interval $(\text{natAdd}\ m\ i, \text{natAdd}\ m\ j]$. In other words: $$\text{map}(\text{natAddEmb}\ m)((i, j]) = (\text{natAdd}\ m\ i, \text{natAdd}\ m\ j]$$

Fin.map_natAddEmb_Ioo theorem

(m) (i j : Fin n) : (Ioo i j).map (natAddEmb m) = Ioo (natAdd m i) (natAdd m j)

Full source

@[simp]
theorem map_natAddEmb_Ioo (m) (i j : Fin n) :
    (Ioo i j).map (natAddEmb m) = Ioo (natAdd m i) (natAdd m j) := by
  simp [← coe_inj]

Image of Open Interval under $\text{natAddEmb}(m)$ in Finite Types

Informal description

For any natural number $m$ and elements $i, j$ in $\text{Fin}\ n$, the image of the open interval $(i, j)$ under the embedding $\text{natAddEmb}\ m : \text{Fin}\ n \to \text{Fin}\ (m + n)$ is equal to the open interval $(\text{natAdd}\ m\ i, \text{natAdd}\ m\ j)$. In other words: $$\text{map}\ (\text{natAddEmb}\ m)\ (i, j) = (\text{natAdd}\ m\ i, \text{natAdd}\ m\ j)$$

Fin.map_natAddEmb_uIcc theorem

(m) (i j : Fin n) : (uIcc i j).map (natAddEmb m) = uIcc (natAdd m i) (natAdd m j)

Full source

@[simp]
theorem map_natAddEmb_uIcc (m) (i j : Fin n) :
    (uIcc i j).map (natAddEmb m) = uIcc (natAdd m i) (natAdd m j) := by
  simp [← coe_inj]

Image of Unordered Closed Interval under `natAddEmb` in Finite Types

Informal description

For any natural number $m$ and any elements $i, j$ in $\text{Fin}\ n$, the image of the unordered closed interval $[i \sqcap j, i \sqcup j]$ under the embedding $\text{natAddEmb}\ m : \text{Fin}\ n \to \text{Fin}\ (m + n)$ is equal to the unordered closed interval $[\text{natAdd}\ m\ i \sqcap \text{natAdd}\ m\ j, \text{natAdd}\ m\ i \sqcup \text{natAdd}\ m\ j]$. In other words: $$(\text{uIcc}\ i\ j).\text{map}\ (\text{natAddEmb}\ m) = \text{uIcc}\ (\text{natAdd}\ m\ i)\ (\text{natAdd}\ m\ j)$$

Fin.map_natAddEmb_Ici theorem

(m) (i : Fin n) : (Ici i).map (natAddEmb m) = Ici (natAdd m i)

Full source

@[simp]
theorem map_natAddEmb_Ici (m) (i : Fin n) : (Ici i).map (natAddEmb m) = Ici (natAdd m i) := by
  simp [← coe_inj]

Image of Left-Closed Interval under `natAddEmb` in Finite Types

Informal description

For any natural number $m$ and any element $i$ in $\text{Fin}\ n$, the image of the left-closed right-infinite interval $[i, \infty)$ under the embedding $\text{natAddEmb}\ m : \text{Fin}\ n \to \text{Fin}\ (m + n)$ is equal to the left-closed right-infinite interval $[\text{natAdd}\ m\ i, \infty)$. In other words: $$\text{natAddEmb}\ m([i, \infty)) = [\text{natAdd}\ m\ i, \infty)$$

Fin.map_natAddEmb_Ioi theorem

(m) (i : Fin n) : (Ioi i).map (natAddEmb m) = Ioi (natAdd m i)

Full source

@[simp]
theorem map_natAddEmb_Ioi (m) (i : Fin n) : (Ioi i).map (natAddEmb m) = Ioi (natAdd m i) := by
  simp [← coe_inj]

Image of Open Interval under `natAddEmb` in Finite Types

Informal description

For any natural number $m$ and any element $i$ in $\text{Fin}\ n$, the image of the open interval $(i, \infty)$ under the embedding $\text{natAddEmb}\ m : \text{Fin}\ n \to \text{Fin}\ (m + n)$ is equal to the open interval $(\text{natAdd}\ m\ i, \infty)$. In other words: $$(\text{Ioi}\ i).\text{map}\ (\text{natAddEmb}\ m) = \text{Ioi}\ (\text{natAdd}\ m\ i)$$

Fin.finsetImage_addNat_Icc theorem

(m) (i j : Fin n) : (Icc i j).image (addNat · m) = Icc (i.addNat m) (j.addNat m)

Full source

@[simp]
theorem finsetImage_addNat_Icc (m) (i j : Fin n) :
    (Icc i j).image (addNat · m) = Icc (i.addNat m) (j.addNat m) := by
  simp [← coe_inj]

Image of Closed Interval under Addition in $\mathrm{Fin}\ n$

Informal description

For any natural number $m$ and elements $i, j$ in $\mathrm{Fin}\ n$, the image of the closed interval $[i, j]$ under the function $x \mapsto x + m$ is equal to the closed interval $[i + m, j + m]$. In symbols: $$\{x + m \mid x \in [i, j]\} = [i + m, j + m]$$

Fin.finsetImage_addNat_Ico theorem

(m) (i j : Fin n) : (Ico i j).image (addNat · m) = Ico (i.addNat m) (j.addNat m)

Full source

@[simp]
theorem finsetImage_addNat_Ico (m) (i j : Fin n) :
    (Ico i j).image (addNat · m) = Ico (i.addNat m) (j.addNat m) := by
  simp [← coe_inj]

Image of Shifted Interval under Addition in $\mathrm{Fin}\ n$: $\mathrm{image}(x \mapsto x + m, [i, j)) = [i + m, j + m)$

Informal description

For any natural number $m$ and any elements $i, j$ of $\mathrm{Fin}\ n$, the image of the left-closed right-open interval $[i, j)$ under the function $x \mapsto x + m$ is equal to the left-closed right-open interval $[i + m, j + m)$. In other words: $$\{x + m \mid x \in [i, j)\} = [i + m, j + m)$$

Fin.finsetImage_addNat_Ioc theorem

(m) (i j : Fin n) : (Ioc i j).image (addNat · m) = Ioc (i.addNat m) (j.addNat m)

Full source

@[simp]
theorem finsetImage_addNat_Ioc (m) (i j : Fin n) :
    (Ioc i j).image (addNat · m) = Ioc (i.addNat m) (j.addNat m) := by
  simp [← coe_inj]

Image of Shifted Ioc Interval under Addition in $\mathrm{Fin}\ n$

Informal description

For any natural number $m$ and elements $i, j$ in $\mathrm{Fin}\ n$, the image of the left-open right-closed interval $(i, j]$ under the function $x \mapsto x + m$ is equal to the left-open right-closed interval $(i + m, j + m)$. In other words: $$\{x + m \mid x \in (i, j]\} = (i + m, j + m]$$

Fin.finsetImage_addNat_Ioo theorem

(m) (i j : Fin n) : (Ioo i j).image (addNat · m) = Ioo (i.addNat m) (j.addNat m)

Full source

@[simp]
theorem finsetImage_addNat_Ioo (m) (i j : Fin n) :
    (Ioo i j).image (addNat · m) = Ioo (i.addNat m) (j.addNat m) := by
  simp [← coe_inj]

Image of Open Interval under Addition in $\mathrm{Fin}\ n$

Informal description

For any natural number $m$ and elements $i, j$ in $\mathrm{Fin}\ n$, the image of the open interval $(i, j)$ under the function $x \mapsto x + m$ is equal to the open interval $(i + m, j + m)$. In other words: $$\{x + m \mid x \in (i, j)\} = (i + m, j + m)$$

Fin.finsetImage_addNat_uIcc theorem

(m) (i j : Fin n) : (uIcc i j).image (addNat · m) = uIcc (i.addNat m) (j.addNat m)

Full source

@[simp]
theorem finsetImage_addNat_uIcc (m) (i j : Fin n) :
    (uIcc i j).image (addNat · m) = uIcc (i.addNat m) (j.addNat m) := by
  simp [← coe_inj]

Image of Unordered Closed Interval under Addition in $\mathrm{Fin}\ n$

Informal description

For any natural number $m$ and elements $i, j$ in $\mathrm{Fin}\ n$, the image of the unordered closed interval $\mathrm{uIcc}(i, j)$ under the function $x \mapsto x + m$ is equal to the unordered closed interval $\mathrm{uIcc}(i + m, j + m)$. In other words: $$\{x + m \mid x \in \mathrm{Fin}\ n \text{ and } \min(i, j) \leq x \leq \max(i, j)\} = \{y \in \mathrm{Fin}\ n \mid \min(i + m, j + m) \leq y \leq \max(i + m, j + m)\}$$

Fin.finsetImage_addNat_Ici theorem

(m) (i : Fin n) : (Ici i).image (addNat · m) = Ici (i.addNat m)

Full source

@[simp]
theorem finsetImage_addNat_Ici (m) (i : Fin n) : (Ici i).image (addNat · m) = Ici (i.addNat m) := by
  simp [← coe_inj]

Image of Closed-Infinite Interval under $\mathrm{addNat}$ in $\mathrm{Fin}\ n$

Informal description

For any natural number $m$ and any element $i$ in $\mathrm{Fin}\ n$, the image of the closed-infinite interval $[i, \infty)$ under the function $\mathrm{addNat}(\cdot, m)$ is equal to the closed-infinite interval $[i + m, \infty)$. In symbols: $$\mathrm{image}(\mathrm{addNat}(\cdot, m), [i, \infty)) = [i + m, \infty)$$

Fin.finsetImage_addNat_Ioi theorem

(m) (i : Fin n) : (Ioi i).image (addNat · m) = Ioi (i.addNat m)

Full source

@[simp]
theorem finsetImage_addNat_Ioi (m) (i : Fin n) : (Ioi i).image (addNat · m) = Ioi (i.addNat m) := by
  simp [← coe_inj]

Image of Right-Infinite Open Interval under Addition in $\mathrm{Fin}\ n$

Informal description

For any natural number $m$ and any element $i$ in $\mathrm{Fin}\ n$, the image of the open interval $(i, \infty)$ under the function $x \mapsto x + m$ is equal to the open interval $(i + m, \infty)$. In other words: $$\{x + m \mid x \in \mathrm{Fin}\ n \text{ and } x > i\} = \{y \in \mathrm{Fin}\ n \mid y > i + m\}$$

Fin.map_addNatEmb_Icc theorem

(m) (i j : Fin n) : (Icc i j).map (addNatEmb m) = Icc (i.addNat m) (j.addNat m)

Full source

@[simp]
theorem map_addNatEmb_Icc (m) (i j : Fin n) :
    (Icc i j).map (addNatEmb m) = Icc (i.addNat m) (j.addNat m) := by
  simp [← coe_inj]

Image of Closed Interval under Addition Embedding in $\mathrm{Fin}\ n$

Informal description

For any natural number $m$ and elements $i, j$ in $\mathrm{Fin}\ n$, the image of the closed interval $[i, j]$ under the embedding $x \mapsto x + m$ is equal to the closed interval $[i + m, j + m]$. In other words: $$\{x + m \mid x \in \mathrm{Fin}\ n \text{ and } i \leq x \leq j\} = \{y \in \mathrm{Fin}\ n \mid i + m \leq y \leq j + m\}$$

Fin.map_addNatEmb_Ico theorem

(m) (i j : Fin n) : (Ico i j).map (addNatEmb m) = Ico (i.addNat m) (j.addNat m)

Full source

@[simp]
theorem map_addNatEmb_Ico (m) (i j : Fin n) :
    (Ico i j).map (addNatEmb m) = Ico (i.addNat m) (j.addNat m) := by
  simp [← coe_inj]

Image of Shifted Interval under Addition Embedding in $\mathrm{Fin}\ n$

Informal description

For any natural number $m$ and any elements $i, j$ of $\mathrm{Fin}\ n$, the image of the left-closed right-open interval $[i, j)$ under the embedding $x \mapsto x + m$ is equal to the left-closed right-open interval $[i + m, j + m)$. In other words: $$\{x + m \mid x \in [i, j)\} = [i + m, j + m)$$

Fin.map_addNatEmb_Ioc theorem

(m) (i j : Fin n) : (Ioc i j).map (addNatEmb m) = Ioc (i.addNat m) (j.addNat m)

Full source

@[simp]
theorem map_addNatEmb_Ioc (m) (i j : Fin n) :
    (Ioc i j).map (addNatEmb m) = Ioc (i.addNat m) (j.addNat m) := by
  simp [← coe_inj]

Image of Shifted Ioc Interval under Addition Embedding in $\mathrm{Fin}\ n$

Informal description

For any natural number $m$ and elements $i, j$ in $\mathrm{Fin}\ n$, the image of the left-open right-closed interval $(i, j]$ under the embedding $x \mapsto x + m$ is equal to the left-open right-closed interval $(i + m, j + m]$. In other words: $$\{x + m \mid x \in \mathrm{Fin}\ n \text{ and } i < x \leq j\} = \{y \in \mathrm{Fin}\ n \mid i + m < y \leq j + m\}$$

Fin.map_addNatEmb_Ioo theorem

(m) (i j : Fin n) : (Ioo i j).map (addNatEmb m) = Ioo (i.addNat m) (j.addNat m)

Full source

@[simp]
theorem map_addNatEmb_Ioo (m) (i j : Fin n) :
    (Ioo i j).map (addNatEmb m) = Ioo (i.addNat m) (j.addNat m) := by
  simp [← coe_inj]

Image of Open Interval under Addition Embedding in $\mathrm{Fin}\ n$

Informal description

For any natural number $m$ and elements $i, j$ of $\mathrm{Fin}\ n$, the image of the open interval $(i, j)$ under the embedding $x \mapsto x + m$ is equal to the open interval $(i + m, j + m)$. In other words: $$\mathrm{map}\ (x \mapsto x + m)\ (i, j) = (i + m, j + m)$$

Fin.map_addNatEmb_uIcc theorem

(m) (i j : Fin n) : (uIcc i j).map (addNatEmb m) = uIcc (i.addNat m) (j.addNat m)

Full source

@[simp]
theorem map_addNatEmb_uIcc (m) (i j : Fin n) :
    (uIcc i j).map (addNatEmb m) = uIcc (i.addNat m) (j.addNat m) := by
  simp [← coe_inj]

Image of Unordered Closed Interval under Addition Embedding in $\mathrm{Fin}\ n$

Informal description

For any natural number $m$ and elements $i, j$ in $\mathrm{Fin}\ n$, the image of the unordered closed interval $\mathrm{uIcc}(i, j)$ under the embedding $x \mapsto x + m$ is equal to the unordered closed interval $\mathrm{uIcc}(i + m, j + m)$. In other words: $$\{x + m \mid x \in \mathrm{Fin}\ n \text{ and } \min(i, j) \leq x \leq \max(i, j)\} = \{y \in \mathrm{Fin}\ n \mid \min(i + m, j + m) \leq y \leq \max(i + m, j + m)\}$$

Fin.map_addNatEmb_Ici theorem

(m) (i : Fin n) : (Ici i).map (addNatEmb m) = Ici (i.addNat m)

Full source

@[simp]
theorem map_addNatEmb_Ici (m) (i : Fin n) : (Ici i).map (addNatEmb m) = Ici (i.addNat m) := by
  simp [← coe_inj]

Image of Closed-Infinite Interval under $\mathrm{addNatEmb}$ Operation in $\mathrm{Fin}\ n$

Informal description

For any natural number $m$ and any element $i$ of $\mathrm{Fin}\ n$, the image of the closed-infinite interval $[i, \infty)$ under the embedding $\mathrm{addNatEmb}(m)$ is equal to the closed-infinite interval $[i + m, \infty)$. In other words: $$\mathrm{addNatEmb}(m)([i, \infty)) = [i + m, \infty)$$

Fin.map_addNatEmb_Ioi theorem

(m) (i : Fin n) : (Ioi i).map (addNatEmb m) = Ioi (i.addNat m)

Full source

@[simp]
theorem map_addNatEmb_Ioi (m) (i : Fin n) : (Ioi i).map (addNatEmb m) = Ioi (i.addNat m) := by
  simp [← coe_inj]

Image of Right-Infinite Open Interval under Addition Embedding in $\mathrm{Fin}\ n$

Informal description

For any natural number $m$ and any element $i$ of $\mathrm{Fin}\ n$, the image of the open interval $(i, \infty)$ under the embedding $x \mapsto x + m$ is equal to the open interval $(i + m, \infty)$. In other words: $$\{x + m \mid x \in \mathrm{Fin}\ n \text{ and } x > i\} = \{y \in \mathrm{Fin}\ n \mid y > i + m\}$$

Fin.finsetImage_succ_Icc theorem

(i j : Fin n) : (Icc i j).image succ = Icc i.succ j.succ

Full source

@[simp]
theorem finsetImage_succ_Icc (i j : Fin n) : (Icc i j).image succ = Icc i.succ j.succ :=
  finsetImage_addNat_Icc ..

Image of Closed Interval under Successor in $\mathrm{Fin}\ n$

Informal description

For any elements $i, j$ in $\mathrm{Fin}\ n$, the image of the closed interval $[i, j]$ under the successor function is equal to the closed interval $[i+1, j+1]$. In symbols: $$\{x+1 \mid x \in [i, j]\} = [i+1, j+1]$$

Fin.finsetImage_succ_Ico theorem

(i j : Fin n) : (Ico i j).image succ = Ico i.succ j.succ

Full source

@[simp]
theorem finsetImage_succ_Ico (i j : Fin n) : (Ico i j).image succ = Ico i.succ j.succ :=
  finsetImage_addNat_Ico ..

Image of Interval under Successor in $\mathrm{Fin}\ n$: $\mathrm{image}(\mathrm{succ}, [i, j)) = [\mathrm{succ}(i), \mathrm{succ}(j))$

Informal description

For any elements $i, j$ of $\mathrm{Fin}\ n$, the image of the left-closed right-open interval $[i, j)$ under the successor function $\mathrm{succ}$ is equal to the left-closed right-open interval $[\mathrm{succ}(i), \mathrm{succ}(j))$. In other words: $$\{\mathrm{succ}(x) \mid x \in [i, j)\} = [\mathrm{succ}(i), \mathrm{succ}(j))$$

Fin.finsetImage_succ_Ioc theorem

(i j : Fin n) : (Ioc i j).image succ = Ioc i.succ j.succ

Full source

@[simp]
theorem finsetImage_succ_Ioc (i j : Fin n) : (Ioc i j).image succ = Ioc i.succ j.succ :=
  finsetImage_addNat_Ioc ..

Image of Shifted Ioc Interval under Successor in $\mathrm{Fin}\ n$

Informal description

For any elements $i, j$ in $\mathrm{Fin}\ n$, the image of the left-open right-closed interval $(i, j]$ under the successor function is equal to the left-open right-closed interval $(i + 1, j + 1]$. In other words: $$\{x + 1 \mid x \in (i, j]\} = (i + 1, j + 1]$$

Fin.finsetImage_succ_Ioo theorem

(i j : Fin n) : (Ioo i j).image succ = Ioo i.succ j.succ

Full source

@[simp]
theorem finsetImage_succ_Ioo (i j : Fin n) : (Ioo i j).image succ = Ioo i.succ j.succ :=
  finsetImage_addNat_Ioo ..

Image of Open Interval under Successor in $\mathrm{Fin}\ n$

Informal description

For any elements $i, j$ in $\mathrm{Fin}\ n$, the image of the open interval $(i, j)$ under the successor function $\mathrm{succ}$ is equal to the open interval $(i.\mathrm{succ}, j.\mathrm{succ})$. In other words: $$\{\mathrm{succ}(x) \mid x \in (i, j)\} = (i.\mathrm{succ}, j.\mathrm{succ})$$

Fin.finsetImage_succ_uIcc theorem

(i j : Fin n) : (uIcc i j).image succ = uIcc i.succ j.succ

Full source

@[simp]
theorem finsetImage_succ_uIcc (i j : Fin n) : (uIcc i j).image succ = uIcc i.succ j.succ :=
  finsetImage_addNat_uIcc ..

Successor Preserves Unordered Closed Intervals in $\mathrm{Fin}\ n$

Informal description

For any elements $i, j$ in $\mathrm{Fin}\ n$, the image of the unordered closed interval $\mathrm{uIcc}(i, j)$ under the successor function is equal to the unordered closed interval $\mathrm{uIcc}(i + 1, j + 1)$. In other words: $$\{x + 1 \mid x \in \mathrm{Fin}\ n \text{ and } \min(i, j) \leq x \leq \max(i, j)\} = \{y \in \mathrm{Fin}\ n \mid \min(i + 1, j + 1) \leq y \leq \max(i + 1, j + 1)\}$$

Fin.finsetImage_succ_Ici theorem

(i : Fin n) : (Ici i).image succ = Ici i.succ

Full source

@[simp]
theorem finsetImage_succ_Ici (i : Fin n) : (Ici i).image succ = Ici i.succ :=
  finsetImage_addNat_Ici ..

Image of Closed-Infinite Interval under Successor in $\mathrm{Fin}\ n$

Informal description

For any element $i$ in $\mathrm{Fin}\ n$, the image of the closed-infinite interval $[i, \infty)$ under the successor function $\mathrm{succ}$ is equal to the closed-infinite interval $[\mathrm{succ}(i), \infty)$. In symbols: $$\mathrm{succ}([i, \infty)) = [\mathrm{succ}(i), \infty)$$

Fin.finsetImage_succ_Ioi theorem

(i : Fin n) : (Ioi i).image succ = Ioi i.succ

Full source

@[simp]
theorem finsetImage_succ_Ioi (i : Fin n) : (Ioi i).image succ = Ioi i.succ :=
  finsetImage_addNat_Ioi ..

Successor Preserves Right-Infinite Open Intervals in $\mathrm{Fin}\ n$

Informal description

For any element $i$ in $\mathrm{Fin}\ n$, the image of the open interval $(i, \infty)$ under the successor function $\mathrm{succ}$ is equal to the open interval $(\mathrm{succ}(i), \infty)$. In symbols: $$\mathrm{succ}\big((i, \infty)\big) = (\mathrm{succ}(i), \infty)$$

Fin.finsetImage_succ_Iic theorem

(i : Fin n) : (Iic i).image succ = Ioc 0 i.succ

Full source

@[simp]
theorem finsetImage_succ_Iic (i : Fin n) : (Iic i).image succ = Ioc 0 i.succ := by
  simp [← coe_inj]

Image of Closed Interval under Successor in Finite Ordinals

Informal description

For any finite ordinal $i \in \text{Fin } n$, the image of the closed interval $(-\infty, i]$ under the successor operation $\text{succ}$ is equal to the left-open right-closed interval $(0, i.\text{succ}]$. In symbols: $$\text{succ}''\, (-\infty, i] = (0, i.\text{succ}]$$

Fin.finsetImage_succ_Iio theorem

(i : Fin n) : (Iio i).image succ = Ioo 0 i.succ

Full source

@[simp]
theorem finsetImage_succ_Iio (i : Fin n) : (Iio i).image succ = Ioo 0 i.succ := by
  simp [← coe_inj]

Image of Left-infinite Interval under Successor in Finite Types

Informal description

For any element $i$ in $\operatorname{Fin} n$, the image of the open interval $(-\infty, i)$ under the successor function $\operatorname{succ}$ is equal to the open interval $(0, \operatorname{succ}(i))$. In other words: $$\operatorname{succ}(\{x \mid x < i\}) = \{y \mid 0 < y < \operatorname{succ}(i)\}$$

Fin.map_succEmb_Icc theorem

(i j : Fin n) : (Icc i j).map (succEmb n) = Icc i.succ j.succ

Full source

@[simp]
theorem map_succEmb_Icc (i j : Fin n) : (Icc i j).map (succEmb n) = Icc i.succ j.succ :=
  map_addNatEmb_Icc ..

Image of Closed Interval under Successor Embedding in $\mathrm{Fin}\ n$

Informal description

For any elements $i, j$ in $\mathrm{Fin}\ n$, the image of the closed interval $[i, j]$ under the successor embedding $\mathrm{succEmb}\ n$ is equal to the closed interval $[\mathrm{succ}(i), \mathrm{succ}(j)]$. In symbols: $$\mathrm{succEmb}\ n''\, [i, j] = [\mathrm{succ}(i), \mathrm{succ}(j)]$$

Fin.map_succEmb_Ico theorem

(i j : Fin n) : (Ico i j).map (succEmb n) = Ico i.succ j.succ

Full source

@[simp]
theorem map_succEmb_Ico (i j : Fin n) : (Ico i j).map (succEmb n) = Ico i.succ j.succ :=
  map_addNatEmb_Ico ..

Successor Embedding Preserves Half-Open Intervals in $\mathrm{Fin}(n)$

Informal description

For any elements $i, j$ in $\mathrm{Fin}(n)$, the image of the half-open interval $[i, j)$ under the successor embedding $\mathrm{succEmb}$ is equal to the half-open interval $[\mathrm{succ}(i), \mathrm{succ}(j))$. In other words: $$\mathrm{succEmb}([i, j)) = [\mathrm{succ}(i), \mathrm{succ}(j))$$

Fin.map_succEmb_Ioc theorem

(i j : Fin n) : (Ioc i j).map (succEmb n) = Ioc i.succ j.succ

Full source

@[simp]
theorem map_succEmb_Ioc (i j : Fin n) : (Ioc i j).map (succEmb n) = Ioc i.succ j.succ :=
  map_addNatEmb_Ioc ..

Successor Embedding Preserves Left-Open Right-Closed Intervals in $\mathrm{Fin}(n)$

Informal description

For any elements $i, j$ in $\mathrm{Fin}(n)$, the image of the left-open right-closed interval $(i, j]$ under the successor embedding $\mathrm{succEmb}$ is equal to the left-open right-closed interval $(\mathrm{succ}(i), \mathrm{succ}(j)]$. In symbols: $$\mathrm{succEmb}((i, j]) = (\mathrm{succ}(i), \mathrm{succ}(j)]$$

Fin.map_succEmb_Ioo theorem

(i j : Fin n) : (Ioo i j).map (succEmb n) = Ioo i.succ j.succ

Full source

@[simp]
theorem map_succEmb_Ioo (i j : Fin n) : (Ioo i j).map (succEmb n) = Ioo i.succ j.succ :=
  map_addNatEmb_Ioo ..

Successor Embedding Preserves Open Intervals in $\mathrm{Fin}(n)$

Informal description

For any elements $i, j$ in $\mathrm{Fin}(n)$, the image of the open interval $(i, j)$ under the successor embedding $\mathrm{succEmb}$ is equal to the open interval $(\mathrm{succ}(i), \mathrm{succ}(j))$. In other words: $$\mathrm{map}\ \mathrm{succEmb}\ (i, j) = (\mathrm{succ}(i), \mathrm{succ}(j))$$

Fin.map_succEmb_uIcc theorem

(i j : Fin n) : (uIcc i j).map (succEmb n) = uIcc i.succ j.succ

Full source

@[simp]
theorem map_succEmb_uIcc (i j : Fin n) : (uIcc i j).map (succEmb n) = uIcc i.succ j.succ :=
  map_addNatEmb_uIcc ..

Successor Embedding Preserves Unordered Closed Intervals in $\mathrm{Fin}(n)$

Informal description

For any elements $i, j$ in $\mathrm{Fin}(n)$, the image of the unordered closed interval $\mathrm{uIcc}(i, j)$ under the successor embedding $\mathrm{succEmb}$ is equal to the unordered closed interval $\mathrm{uIcc}(i.\mathrm{succ}, j.\mathrm{succ})$. In other words: $$\{x.\mathrm{succ} \mid x \in \mathrm{Fin}(n) \text{ and } \min(i, j) \leq x \leq \max(i, j)\} = \{y \in \mathrm{Fin}(n) \mid \min(i.\mathrm{succ}, j.\mathrm{succ}) \leq y \leq \max(i.\mathrm{succ}, j.\mathrm{succ})\}$$

Fin.map_succEmb_Ici theorem

(i : Fin n) : (Ici i).map (succEmb n) = Ici i.succ

Full source

@[simp]
theorem map_succEmb_Ici (i : Fin n) : (Ici i).map (succEmb n) = Ici i.succ :=
  map_addNatEmb_Ici ..

Image of Closed-Infinite Interval under Successor Embedding in $\text{Fin}(n)$

Informal description

For any element $i$ in $\text{Fin}(n)$, the image of the closed-infinite interval $[i, \infty)$ under the successor embedding $\text{succEmb}(n)$ is equal to the closed-infinite interval $[i.\text{succ}, \infty)$. In symbols: $$\text{succEmb}(n)([i, \infty)) = [i.\text{succ}, \infty)$$

Fin.map_succEmb_Ioi theorem

(i : Fin n) : (Ioi i).map (succEmb n) = Ioi i.succ

Full source

@[simp]
theorem map_succEmb_Ioi (i : Fin n) : (Ioi i).map (succEmb n) = Ioi i.succ :=
  map_addNatEmb_Ioi ..

Image of Right-Infinite Open Interval under Successor Embedding in $\text{Fin}(n)$

Informal description

For any element $i$ in $\text{Fin}(n)$, the image of the open interval $(i, \infty)$ under the successor embedding $\text{succEmb}$ is equal to the open interval $(i.\text{succ}, \infty)$. In symbols: $$\text{succEmb}((i, \infty)) = (i.\text{succ}, \infty)$$

Fin.map_succEmb_Iic theorem

(i : Fin n) : (Iic i).map (succEmb n) = Ioc 0 i.succ

Full source

@[simp]
theorem map_succEmb_Iic (i : Fin n) : (Iic i).map (succEmb n) = Ioc 0 i.succ := by
  simp [← coe_inj]

Image of Closed Interval under Successor Embedding in Finite Ordinals

Informal description

For any finite ordinal $i \in \text{Fin } n$, the image of the closed interval $(-\infty, i]$ under the successor embedding $\text{succEmb}$ is equal to the left-open right-closed interval $(0, i.\text{succ}]$. In symbols: $$\text{succEmb}((-\infty, i]) = (0, i.\text{succ}]$$

Fin.map_succEmb_Iio theorem

(i : Fin n) : (Iio i).map (succEmb n) = Ioo 0 i.succ

Full source

@[simp]
theorem map_succEmb_Iio (i : Fin n) : (Iio i).map (succEmb n) = Ioo 0 i.succ := by
  simp [← coe_inj]

Image of Left-infinite Interval under Successor Embedding in Finite Types

Informal description

For any element $i$ in $\operatorname{Fin} n$, the image of the open interval $(-\infty, i)$ under the successor embedding $\operatorname{succEmb}$ is equal to the open interval $(0, \operatorname{succ}(i))$. In other words: $$(\operatorname{succEmb} n)(\{x \mid x < i\}) = \{y \mid 0 < y < \operatorname{succ}(i)\}$$

Fin.finsetImage_rev_Icc theorem

(i j : Fin n) : (Icc i j).image rev = Icc j.rev i.rev

Full source

@[simp]
theorem finsetImage_rev_Icc (i j : Fin n) : (Icc i j).image rev = Icc j.rev i.rev := by
  simp [← coe_inj]

Image of Closed Interval under Reverse Operation in Finite Types

Informal description

For any two elements $i$ and $j$ in $\text{Fin}\,n$, the image of the closed interval $[i, j]$ under the reverse operation $\text{rev}$ is equal to the closed interval $[\text{rev}\,j, \text{rev}\,i]$.

Fin.finsetImage_rev_Ico theorem

(i j : Fin n) : (Ico i j).image rev = Ioc j.rev i.rev

Full source

@[simp]
theorem finsetImage_rev_Ico (i j : Fin n) : (Ico i j).image rev = Ioc j.rev i.rev := by
  simp [← coe_inj]

Image of $\text{Ico}(i, j)$ under Reverse Operation in $\text{Fin}\,n$ Equals $\text{Ioc}(j^{\text{rev}}, i^{\text{rev}})$

Informal description

For any two elements $i$ and $j$ in $\text{Fin}\,n$, the image of the left-closed right-open interval $\text{Ico}(i, j)$ under the reverse operation $\text{rev}$ is equal to the left-open right-closed interval $\text{Ioc}(j^{\text{rev}}, i^{\text{rev}})$. That is, \[ \text{rev}(\text{Ico}(i, j)) = \text{Ioc}(j^{\text{rev}}, i^{\text{rev}}), \] where $i^{\text{rev}}$ and $j^{\text{rev}}$ are the reverses of $i$ and $j$ respectively.

Fin.finsetImage_rev_Ioc theorem

(i j : Fin n) : (Ioc i j).image rev = Ico j.rev i.rev

Full source

@[simp]
theorem finsetImage_rev_Ioc (i j : Fin n) : (Ioc i j).image rev = Ico j.rev i.rev := by
  simp [← coe_inj]

Image of Open-Closed Interval under Finite Reverse Operation Equals Closed-Open Interval of Reversed Endpoints

Informal description

For any two elements $i$ and $j$ in $\text{Fin}\,n$, the image of the open-closed interval $(i, j]$ under the reverse operation $\text{rev}$ equals the closed-open interval $[j^{\text{rev}}, i^{\text{rev}})$, where $i^{\text{rev}}$ and $j^{\text{rev}}$ are the reverses of $i$ and $j$ respectively.

Fin.finsetImage_rev_Ioo theorem

(i j : Fin n) : (Ioo i j).image rev = Ioo j.rev i.rev

Full source

@[simp]
theorem finsetImage_rev_Ioo (i j : Fin n) : (Ioo i j).image rev = Ioo j.rev i.rev := by
  simp [← coe_inj]

Image of Open Interval under Reverse Operation in $\text{Fin}(n)$

Informal description

For any two elements $i$ and $j$ in $\text{Fin}\,n$, the image of the open interval $(i, j)$ under the reverse operation $\text{rev}$ is equal to the open interval $(j.\text{rev}, i.\text{rev})$. That is, $\text{rev}[(i, j)] = (j.\text{rev}, i.\text{rev})$.

Fin.finsetImage_rev_uIcc theorem

(i j : Fin n) : (uIcc i j).image rev = uIcc i.rev j.rev

Full source

@[simp]
theorem finsetImage_rev_uIcc (i j : Fin n) : (uIcc i j).image rev = uIcc i.rev j.rev := by
  simp [← coe_inj]

Image of Unordered Closed Interval under Reverse Operation in $\text{Fin}(n)$

Informal description

For any two elements $i$ and $j$ in $\text{Fin}\,n$, the image of the unordered closed interval $\text{uIcc}(i, j)$ under the reverse operation $\text{rev}$ is equal to the unordered closed interval $\text{uIcc}(i^{\text{rev}}, j^{\text{rev}})$. In other words, $\text{rev}[\text{uIcc}(i, j)] = \text{uIcc}(i^{\text{rev}}, j^{\text{rev}})$.

Fin.finsetImage_rev_Ici theorem

(i : Fin n) : (Ici i).image rev = Iic i.rev

Full source

@[simp]
theorem finsetImage_rev_Ici (i : Fin n) : (Ici i).image rev = Iic i.rev := by simp [← coe_inj]

Image of $[i, \infty)$ under Finite Reverse Operation Equals $(-\infty, \text{rev}(i)]$

Informal description

For any finite ordinal $i \in \text{Fin}\,n$, the image of the left-closed right-infinite interval $[i, \infty)$ under the reverse operation $\text{rev}$ is equal to the left-infinite right-closed interval $(-\infty, \text{rev}(i)]$. In other words, $\text{image}(\text{rev}, [i, \infty)) = (-\infty, \text{rev}(i)]$.

Fin.finsetImage_rev_Ioi theorem

(i : Fin n) : (Ioi i).image rev = Iio i.rev

Full source

@[simp]
theorem finsetImage_rev_Ioi (i : Fin n) : (Ioi i).image rev = Iio i.rev := by simp [← coe_inj]

Image of Upper Interval under Reverse Operation in Finite Ordinals: $\text{rev}[(i, \infty)] = (-\infty, \text{rev}(i))$

Informal description

For any element $i$ in $\text{Fin}\,n$, the image of the open upper interval $(i, \infty)$ under the reverse operation $\text{rev}$ is equal to the open lower interval $(-\infty, \text{rev}(i))$.

Fin.finsetImage_rev_Iic theorem

(i : Fin n) : (Iic i).image rev = Ici i.rev

Full source

@[simp]
theorem finsetImage_rev_Iic (i : Fin n) : (Iic i).image rev = Ici i.rev := by simp [← coe_inj]

Image of Lower-Closed Interval under Finite Reverse Operation Equals Closed-Infinite Interval of Reverse

Informal description

For any element $i$ in $\text{Fin}\,n$, the image of the lower-closed interval $(-\infty, i]$ under the reverse operation $\text{rev}$ is equal to the closed-infinite interval $[\text{rev}(i), \infty)$.

Fin.finsetImage_rev_Iio theorem

(i : Fin n) : (Iio i).image rev = Ioi i.rev

Full source

@[simp]
theorem finsetImage_rev_Iio (i : Fin n) : (Iio i).image rev = Ioi i.rev := by simp [← coe_inj]

Image of Open Lower Interval under Reversal in Finite Type

Informal description

For any element $i$ in $\operatorname{Fin}(n)$, the image of the open lower interval $(-\infty, i)$ under the reversal operation $\operatorname{rev}$ is equal to the open upper interval $(i.\operatorname{rev}, \infty)$.

Fin.map_revPerm_Icc theorem

(i j : Fin n) : (Icc i j).map revPerm.toEmbedding = Icc j.rev i.rev

Full source

@[simp]
theorem map_revPerm_Icc (i j : Fin n) : (Icc i j).map revPerm.toEmbedding = Icc j.rev i.rev := by
  simp [← coe_inj]

Image of Closed Interval under Reverse Permutation in Finite Types

Informal description

For any two elements $i$ and $j$ in $\text{Fin}\,n$, the image of the closed interval $[i, j]$ under the reverse permutation $\text{revPerm}$ is equal to the closed interval $[\text{rev}\,j, \text{rev}\,i]$.

Fin.map_revPerm_Ico theorem

(i j : Fin n) : (Ico i j).map revPerm.toEmbedding = Ioc j.rev i.rev

Full source

@[simp]
theorem map_revPerm_Ico (i j : Fin n) : (Ico i j).map revPerm.toEmbedding = Ioc j.rev i.rev := by
  simp [← coe_inj]

Image of Closed-Open Interval under Reverse Permutation in $\text{Fin}\,n$

Informal description

For any two elements $i$ and $j$ in $\text{Fin}\,n$, the image of the closed-open interval $\text{Ico}(i, j)$ under the reverse permutation map $\text{revPerm}$ is equal to the open-closed interval $\text{Ioc}(j^{\text{rev}}, i^{\text{rev}})$, where $i^{\text{rev}}$ and $j^{\text{rev}}$ are the reverses of $i$ and $j$ respectively. That is, \[ \text{revPerm}(\text{Ico}(i, j)) = \text{Ioc}(j^{\text{rev}}, i^{\text{rev}}). \]

Fin.map_revPerm_Ioc theorem

(i j : Fin n) : (Ioc i j).map revPerm.toEmbedding = Ico j.rev i.rev

Full source

@[simp]
theorem map_revPerm_Ioc (i j : Fin n) : (Ioc i j).map revPerm.toEmbedding = Ico j.rev i.rev := by
  simp [← coe_inj]

Image of Open-Closed Interval under Reverse Permutation Equals Closed-Open Interval of Reversed Endpoints

Informal description

For any two elements $i$ and $j$ in $\text{Fin}\,n$, the image of the open-closed interval $(i, j]$ under the reverse permutation map $\text{revPerm}$ is equal to the closed-open interval $[j^{\text{rev}}, i^{\text{rev}})$, where $i^{\text{rev}}$ and $j^{\text{rev}}$ are the reverses of $i$ and $j$ respectively.

Fin.map_revPerm_Ioo theorem

(i j : Fin n) : (Ioo i j).map revPerm.toEmbedding = Ioo j.rev i.rev

Full source

@[simp]
theorem map_revPerm_Ioo (i j : Fin n) : (Ioo i j).map revPerm.toEmbedding = Ioo j.rev i.rev := by
  simp [← coe_inj]

Image of Open Interval under Reverse Permutation in $\text{Fin}\,n$

Informal description

For any two elements $i$ and $j$ in $\text{Fin}\,n$, the image of the open interval $(i, j)$ under the reverse permutation map $\text{revPerm}$ is equal to the open interval $(j^{\text{rev}}, i^{\text{rev}})$, where $i^{\text{rev}}$ and $j^{\text{rev}}$ are the reverses of $i$ and $j$ respectively. That is, \[ \text{revPerm}((i, j)) = (j^{\text{rev}}, i^{\text{rev}}). \]

Fin.map_revPerm_uIcc theorem

(i j : Fin n) : (uIcc i j).map revPerm.toEmbedding = uIcc i.rev j.rev

Full source

@[simp]
theorem map_revPerm_uIcc (i j : Fin n) : (uIcc i j).map revPerm.toEmbedding = uIcc i.rev j.rev := by
  simp [← coe_inj]

Image of Unordered Closed Interval under Reverse Permutation in $\text{Fin}\,n$

Informal description

For any two elements $i$ and $j$ in $\text{Fin}\,n$, the image of the unordered closed interval $\text{uIcc}(i, j)$ under the reverse permutation map $\text{revPerm}$ is equal to the unordered closed interval $\text{uIcc}(i^{\text{rev}}, j^{\text{rev}})$, where $i^{\text{rev}}$ and $j^{\text{rev}}$ are the reverses of $i$ and $j$ respectively. That is, \[ \text{revPerm}(\text{uIcc}(i, j)) = \text{uIcc}(i^{\text{rev}}, j^{\text{rev}}). \]

Fin.map_revPerm_Ici theorem

(i : Fin n) : (Ici i).map revPerm.toEmbedding = Iic i.rev

Full source

@[simp]
theorem map_revPerm_Ici (i : Fin n) : (Ici i).map revPerm.toEmbedding = Iic i.rev := by
  simp [← coe_inj]

Image of $[i, \infty)$ under Reverse Permutation Equals $(-\infty, \text{rev}(i)]$ in $\text{Fin}\,n$

Informal description

For any element $i$ in $\text{Fin}\,n$, the image of the closed-infinite interval $[i, \infty)$ under the reverse permutation $\text{revPerm}$ is equal to the closed lower interval $(-\infty, \text{rev}(i)]$.

Fin.map_revPerm_Ioi theorem

(i : Fin n) : (Ioi i).map revPerm.toEmbedding = Iio i.rev

Full source

@[simp]
theorem map_revPerm_Ioi (i : Fin n) : (Ioi i).map revPerm.toEmbedding = Iio i.rev := by
  simp [← coe_inj]

Image of $(i, \infty)$ under Finite Reverse Permutation Equals $(-\infty, \text{rev}(i))$

Informal description

For any finite ordinal $i \in \text{Fin}\,n$, the image of the open right-infinite interval $(i, \infty)$ under the reverse permutation map $\text{revPerm}$ is equal to the open left-infinite interval $(-\infty, \text{rev}(i))$.

Fin.map_revPerm_Iic theorem

(i : Fin n) : (Iic i).map revPerm.toEmbedding = Ici i.rev

Full source

@[simp]
theorem map_revPerm_Iic (i : Fin n) : (Iic i).map revPerm.toEmbedding = Ici i.rev := by
  simp [← coe_inj]

Image of Lower-Closed Interval under Finite Reverse Permutation Equals Upper-Closed Interval of Reversed Element

Informal description

For any element $i$ in $\text{Fin}\,n$ (the finite type of natural numbers less than $n$), the image of the lower-closed interval $(-\infty, i]$ under the reverse permutation map $\text{revPerm}$ is equal to the upper-closed interval $[\text{rev}(i), \infty)$.

Fin.map_revPerm_Iio theorem

(i : Fin n) : (Iio i).map revPerm.toEmbedding = Ioi i.rev

Full source

@[simp]
theorem map_revPerm_Iio (i : Fin n) : (Iio i).map revPerm.toEmbedding = Ioi i.rev := by
  simp [← coe_inj]

Image of Open Lower Interval under Reversal Permutation in $\operatorname{Fin}(n)$

Informal description

For any element $i$ in $\operatorname{Fin}(n)$, the image of the open lower interval $(-\infty, i)$ under the reversal permutation $\operatorname{revPerm}$ is equal to the open upper interval $(i.\operatorname{rev}, \infty)$.

Fin.card_Icc theorem

: #(Icc a b) = b + 1 - a

Full source

@[simp]
lemma card_Icc : #(Icc a b) = b + 1 - a := by rw [← Nat.card_Icc, ← map_valEmbedding_Icc, card_map]

Cardinality of Closed Interval in $\text{Fin}(n)$: $\#([a, b]) = b + 1 - a$

Informal description

For any two elements $a, b$ in $\text{Fin}(n)$, the cardinality of the closed interval $[a, b]$ is equal to $b + 1 - a$.

Fin.card_Ico theorem

: #(Ico a b) = b - a

Full source

@[simp]
lemma card_Ico : #(Ico a b) = b - a := by rw [← Nat.card_Ico, ← map_valEmbedding_Ico, card_map]

Cardinality of Half-Open Interval in $\text{Fin}(n)$: $\#([a, b)) = b - a$

Informal description

For any two elements $a, b$ in $\text{Fin}(n)$, the cardinality of the half-open interval $[a, b)$ is equal to $b - a$.

Fin.card_Ioc theorem

: #(Ioc a b) = b - a

Full source

@[simp]
lemma card_Ioc : #(Ioc a b) = b - a := by rw [← Nat.card_Ioc, ← map_valEmbedding_Ioc, card_map]

Cardinality of Open-Closed Interval in $\text{Fin}(n)$: $\#((a, b]) = b - a$

Informal description

For any two elements $a, b$ in $\text{Fin}(n)$, the cardinality of the open-closed interval $(a, b]$ is equal to $b - a$.

Fin.card_Ioo theorem

: #(Ioo a b) = b - a - 1

Full source

@[simp]
lemma card_Ioo : #(Ioo a b) = b - a - 1 := by rw [← Nat.card_Ioo, ← map_valEmbedding_Ioo, card_map]

Cardinality of Open Interval in $\text{Fin}(n)$: $\#((a, b)) = b - a - 1$

Informal description

For any elements $a, b$ in $\text{Fin}(n)$, the cardinality of the open interval $(a, b)$ is equal to $b - a - 1$.

Fin.card_uIcc theorem

: #(uIcc a b) = (b - a : ℤ).natAbs + 1

Full source

@[simp]
theorem card_uIcc : #(uIcc a b) = (b - a : ℤ).natAbs + 1 := by
  rw [← Nat.card_uIcc, ← map_valEmbedding_uIcc, card_map]

Cardinality of Unordered Closed Interval in $\text{Fin}(n)$: $\#(\text{uIcc}(a, b)) = |b - a| + 1$

Informal description

For any two elements $a, b$ in $\text{Fin}(n)$, the cardinality of the unordered closed interval $\text{uIcc}(a, b)$ is equal to the absolute value of $b - a$ plus one, i.e., $\#(\text{uIcc}(a, b)) = |b - a| + 1$.

Fin.card_Ici theorem

: #(Ici a) = n - a

Full source

@[simp]
theorem card_Ici : #(Ici a) = n - a := by
  rw [← attachFin_Ico_eq_Ici, card_attachFin, Nat.card_Ico]

Cardinality of Closed-Infinite Interval in $\text{Fin}(n)$: $\#([a, \infty) \cap \text{Fin}(n)) = n - a$

Informal description

For any element $a$ in $\text{Fin}(n)$, the cardinality of the closed-infinite interval $[a, \infty) \cap \text{Fin}(n)$ is equal to $n - a$. Here, $\text{Fin}(n)$ denotes the set $\{0, 1, \dots, n-1\}$ of natural numbers less than $n$, and $[a, \infty) \cap \text{Fin}(n)$ represents the set $\{x \in \text{Fin}(n) \mid a \leq x\}$.

Fin.card_Ioi theorem

: #(Ioi a) = n - 1 - a

Full source

@[simp]
theorem card_Ioi : #(Ioi a) = n - 1 - a := by
  rw [← card_map, map_valEmbedding_Ioi, Nat.card_Ioo, Nat.sub_right_comm]

Cardinality of Open-Infinite Interval in $\text{Fin}(n)$: $\#((a, \infty) \cap \text{Fin}(n)) = n - 1 - a$

Informal description

For any element $a$ in $\text{Fin}(n)$, the cardinality of the open-infinite interval $(a, \infty) \cap \text{Fin}(n)$ is equal to $n - 1 - a$. Here, $\text{Fin}(n)$ denotes the set $\{0, 1, \dots, n-1\}$ of natural numbers less than $n$, and $(a, \infty) \cap \text{Fin}(n)$ represents the set $\{x \in \text{Fin}(n) \mid a < x\}$.

Fin.card_Iic theorem

: #(Iic b) = b + 1

Full source

@[simp]
theorem card_Iic : #(Iic b) = b + 1 := by rw [← Nat.card_Iic b, ← map_valEmbedding_Iic, card_map]

Cardinality of Lower-Closed Interval in $\text{Fin}(n)$: $\#(\text{Iic}(b)) = b + 1$

Informal description

For any element $b$ in $\text{Fin}(n)$, the cardinality of the lower-closed interval $\text{Iic}(b) = \{x \in \text{Fin}(n) \mid x \leq b\}$ is equal to $b + 1$.

Fin.card_Iio theorem

: #(Iio b) = b

Full source

@[simp]
theorem card_Iio : #(Iio b) = b := by rw [← Nat.card_Iio b, ← map_valEmbedding_Iio, card_map]

Cardinality of Open Lower Interval in $\text{Fin}(n)$: $\#(\text{Iio}(b)) = b$

Informal description

For any element $b$ in $\text{Fin}(n)$, the cardinality of the open lower interval $\text{Iio}(b) = \{x \in \text{Fin}(n) \mid x < b\}$ is equal to $b$.

Fin.card_fintypeIcc theorem

: Fintype.card (Set.Icc a b) = b + 1 - a

Full source

@[deprecated Fintype.card_Icc (since := "2025-03-28")]
theorem card_fintypeIcc : Fintype.card (Set.Icc a b) = b + 1 - a := by simp

Cardinality of Closed Interval in $\text{Fin}(n)$: $\#([a, b]) = b + 1 - a$

Informal description

For any two elements $a, b$ in $\text{Fin}(n)$, the cardinality of the closed interval $[a, b]$ as a fintype is equal to $b + 1 - a$.

Fin.card_fintypeIco theorem

: Fintype.card (Set.Ico a b) = b - a

Full source

@[deprecated Fintype.card_Ico (since := "2025-03-28")]
theorem card_fintypeIco : Fintype.card (Set.Ico a b) = b - a := by simp

Cardinality of Closed-Open Interval in $\text{Fin}(n)$: $\text{card}([a, b)) = b - a$

Informal description

For any two elements $a, b$ in $\text{Fin}(n)$, the cardinality of the closed-open interval $[a, b)$ as a fintype is equal to $b - a$.

Fin.card_fintypeIoc theorem

: Fintype.card (Set.Ioc a b) = b - a

Full source

@[deprecated Fintype.card_Ioc (since := "2025-03-28")]
theorem card_fintypeIoc : Fintype.card (Set.Ioc a b) = b - a := by simp

Cardinality of Open-Closed Interval in $\text{Fin}(n)$ as Fintype: $\text{card}((a, b]) = b - a$

Informal description

For any two elements $a, b$ in $\text{Fin}(n)$, the cardinality of the open-closed interval $(a, b]$ as a fintype is equal to $b - a$.

Fin.card_fintypeIoo theorem

: Fintype.card (Set.Ioo a b) = b - a - 1

Full source

@[deprecated Fintype.card_Ioo (since := "2025-03-28")]
theorem card_fintypeIoo : Fintype.card (Set.Ioo a b) = b - a - 1 := by simp

Cardinality of Open Interval in $\text{Fin}(n)$: $\#((a, b)) = b - a - 1$

Informal description

For any elements $a, b$ in $\text{Fin}(n)$, the cardinality of the open interval $(a, b)$ as a fintype is equal to $b - a - 1$.

Fin.card_fintype_uIcc theorem

: Fintype.card (Set.uIcc a b) = (b - a : ℤ).natAbs + 1

Full source

@[deprecated Fintype.card_uIcc (since := "2025-03-28")]
theorem card_fintype_uIcc : Fintype.card (Set.uIcc a b) = (b - a : ℤ).natAbs + 1 := by simp

Cardinality of Unordered Closed Interval in $\text{Fin}(n)$: $\text{card}([a \sqcap b, a \sqcup b]) = |b - a| + 1$

Informal description

For any two elements $a, b$ in $\text{Fin}(n)$, the cardinality of the unordered closed interval $[a \sqcap b, a \sqcup b]$ as a fintype is equal to the absolute value of $b - a$ plus one, i.e., $\text{card}([a \sqcap b, a \sqcup b]) = |b - a| + 1$.

Fin.card_fintypeIci theorem

: Fintype.card (Set.Ici a) = n - a

Full source

@[deprecated Fintype.card_Ici (since := "2025-03-28")]
theorem card_fintypeIci : Fintype.card (Set.Ici a) = n - a := by simp

Cardinality of Closed-Infinite Interval in $\text{Fin}(n)$: $\#([a, \infty) \cap \text{Fin}(n)) = n - a$

Informal description

For any element $a$ in $\text{Fin}(n)$, the cardinality of the closed-infinite interval $[a, \infty) \cap \text{Fin}(n)$ as a fintype is equal to $n - a$. Here, $\text{Fin}(n)$ denotes the set $\{0, 1, \dots, n-1\}$ of natural numbers less than $n$, and $[a, \infty) \cap \text{Fin}(n)$ represents the set $\{x \in \text{Fin}(n) \mid a \leq x\}$.

Fin.card_fintypeIoi theorem

: Fintype.card (Set.Ioi a) = n - 1 - a

Full source

@[deprecated Fintype.card_Ioi (since := "2025-03-28")]
theorem card_fintypeIoi : Fintype.card (Set.Ioi a) = n - 1 - a := by simp

Cardinality of Open-Infinite Interval in $\text{Fin}(n)$: $\text{card}((a, \infty) \cap \text{Fin}(n)) = n - 1 - a$

Informal description

For any element $a$ in $\text{Fin}(n)$, the cardinality of the open-infinite interval $(a, \infty) \cap \text{Fin}(n)$ as a fintype is equal to $n - 1 - a$. Here, $\text{Fin}(n)$ denotes the set $\{0, 1, \dots, n-1\}$ of natural numbers less than $n$, and $(a, \infty) \cap \text{Fin}(n)$ represents the set $\{x \in \text{Fin}(n) \mid a < x\}$.

Fin.card_fintypeIic theorem

: Fintype.card (Set.Iic b) = b + 1

Full source

@[deprecated Fintype.card_Iic (since := "2025-03-28")]
theorem card_fintypeIic : Fintype.card (Set.Iic b) = b + 1 := by simp

Cardinality of Closed Lower Interval in $\text{Fin}(n)$: $\#(\text{Iic}(b)) = b + 1$

Informal description

For any element $b$ in $\text{Fin}(n)$, the cardinality of the closed lower interval $\text{Iic}(b) = \{x \in \text{Fin}(n) \mid x \leq b\}$ as a fintype is equal to $b + 1$.

Fin.card_fintypeIio theorem

: Fintype.card (Set.Iio b) = b

Full source

@[deprecated Fintype.card_Iio (since := "2025-03-28")]
theorem card_fintypeIio : Fintype.card (Set.Iio b) = b := by simp

Cardinality of Open Lower Interval in $\text{Fin}(n)$: $\#(\text{Iio}(b)) = b$

Informal description

For any element $b$ in $\text{Fin}(n)$, the cardinality of the open lower interval $\text{Iio}(b) = \{x \in \text{Fin}(n) \mid x < b\}$ is equal to $b$.