Physlib.Mathematics.Fin

For any $n \in \mathbb{N}$, given elements $i$ and $x$ in $\{0, 1, \dots, n+1\}$ (represented by $\text{Fin}(n+2)$), this function returns an element in $\{0, 1, \dots, n\}$ (represented by $\text{Fin}(n+1)$). The output is defined as $x$ if $x < i$, and $x - 1$ if $x \geq i$.

For any natural number $n$ and any element $i$ in the set $\{0, 1, \dots, n+1\}$ (represented by $\text{Fin}(n+2)$), the function $\text{predAboveI}$ evaluated at $i$ with pivot $i$ is equal to $i - 1$, where the result is an element of $\text{Fin}(n+1)$.

Let $n$ be a natural number. For any pivot $i \in \{0, 1, \dots, n+1\}$ and any element $x \in \{0, 1, \dots, n\}$, applying the function $\text{predAboveI}(i, \cdot)$ to the value obtained from $\text{succAbove}(i, x)$ returns $x$. Here, $\text{succAbove}(i, x)$ is defined as $x$ if $x < i$ and $x + 1$ if $x \geq i$, while $\text{predAboveI}(i, y)$ is defined as $y$ if $y < i$ and $y - 1$ if $y \geq i$. The identity states: $$\text{predAboveI}(i, \text{succAbove}(i, x)) = x$$

For any natural number $n$ and any elements $i, x \in \text{Fin}(n+2)$, if $i \neq x$, then $\text{Fin.succAbove}_i(\text{predAboveI}_i(x)) = x$. Here, $\text{predAboveI}_i(x)$ is the function that returns $x$ if $x < i$ and $x - 1$ if $x \geq i$. The function $\text{Fin.succAbove}_i(y)$ is the standard map from $\text{Fin}(n+1)$ to $\text{Fin}(n+2)$ that "skips" the index $i$, defined as $y$ if $y < i$ and $y + 1$ if $y \geq i$.

Let $n$ be a natural number. For any elements $i, x \in \text{Fin}(n+2)$ such that $i \neq x$, and any element $y \in \text{Fin}(n+1)$, the following equivalence holds: $$y = \text{predAboveI}_i(x) \iff \text{succAbove}_i(y) = x$$ where $\text{predAboveI}_i(x)$ returns $x$ if $x < i$ and $x - 1$ if $x \geq i$, and $\text{succAbove}_i(y)$ is the function from $\text{Fin}(n+1)$ to $\text{Fin}(n+2)$ that skips $i$, defined as $y$ if $y < i$ and $y + 1$ if $y \geq i$.

For any natural number $n$, let $i$ and $x$ be elements of $\text{Fin}(n+2)$. If the value of $x$ is strictly less than the value of $i$ ($x < i$), then the predecessor of $x$ relative to the pivot $i$, denoted $\text{predAboveI}(i, x)$, is equal to $x$ as an element of $\text{Fin}(n+1)$.

For any natural number $n$ and any two elements $i, x \in \text{Fin}(n+2)$, if $i < x$, then the value of the predecessor of $x$ relative to pivot $i$ is $\text{predAboveI}(i, x) = x - 1$, where the result is an element of $\text{Fin}(n+1)$.

For any natural number $n$, let $i \in \text{Fin}(n+2)$, $j \in \text{Fin}(n+1)$, and $x \in \text{Fin}(n)$. The following equality holds: $$i.\text{succAbove}(j.\text{succAbove}(x)) = (i.\text{succAbove}(j)).\text{succAbove}((\text{predAboveI}(i.\text{succAbove}(j), i)).\text{succAbove}(x))$$ where: - For $k \in \text{Fin}(m+1)$, the function $k.\text{succAbove} : \text{Fin}(m) \to \text{Fin}(m+1)$ is the embedding that "skips" the index $k$, defined by $k.\text{succAbove}(y) = y$ if $y < k$ and $k.\text{succAbove}(y) = y + 1$ if $y \ge k$. - The function $\text{predAboveI}(p, i)$ returns the predecessor of $i$ relative to the pivot $p$, defined as $i$ if $i < p$ and $i - 1$ if $i \ge p$.

For any natural number $n$ and an index $i \in \text{Fin}(n+1)$, this definition provides an equivalence (a bijection) between the finite set $\text{Fin}(n+1) = \{0, 1, \dots, n\}$ and the disjoint union $\text{Fin}(1) \oplus \text{Fin}(n)$. This mapping is constructed such that the specific element $i$ is mapped to the unique element in the left summand $\text{Fin}(1)$, while all other elements $j \in \text{Fin}(n+1)$ where $j \neq i$ are mapped into the right summand $\text{Fin}(n)$.

Let $n$ be a natural number and $i \in \text{Fin}(n+1)$. Let $f_i : \text{Fin}(n+1) \simeq \text{Fin}(1) \oplus \text{Fin}(n)$ be the equivalence that extracts the $i$-th component. Then $f_i(i) = \text{inl}(0)$, where $\text{inl}(0)$ is the unique element of the first summand $\text{Fin}(1)$.

For any natural number $n$ and any index $i \in \text{Fin}(n+1)$, the composition of the inverse of the equivalence $\text{finExtractOne}(i) : \text{Fin}(n+1) \simeq \text{Fin}(1) \oplus \text{Fin}(n)$ with the right-side injection $\text{inr} : \text{Fin}(n) \to \text{Fin}(1) \oplus \text{Fin}(n)$ is equal to the function $i.\text{succAbove} : \text{Fin}(n) \to \text{Fin}(n+1)$, which embeds $\text{Fin}(n)$ into $\text{Fin}(n+1)$ by skipping the index $i$.

Let $n$ be a natural number, $i \in \text{Fin}(n+1)$ be an index, and $x \in \text{Fin}(n)$ be an element. Let $f_i: \text{Fin}(n+1) \simeq \text{Fin}(1) \oplus \text{Fin}(n)$ be the equivalence defined by `finExtractOne`, which extracts the $i$-th component to the left summand. Then the inverse of this equivalence applied to the element $x$ in the right summand is equal to $i.\text{succAbove}(x)$: $$f_i^{-1}(\text{inr } x) = i.\text{succAbove}(x)$$ where $i.\text{succAbove} : \text{Fin}(n) \to \text{Fin}(n+1)$ is the function that embeds $\text{Fin}(n)$ into $\text{Fin}(n+1)$ by skipping the index $i$.

For any natural number $n$ and any index $i \in \text{Fin}(n+1)$, let $f_i : \text{Fin}(n+1) \simeq \text{Fin}(1) \oplus \text{Fin}(n)$ be the equivalence (bijection) defined by `finExtractOne`, which maps the element $i$ to the left summand. The inverse of this equivalence applied to the unique element $0 \in \text{Fin}(1)$ in the left summand returns the original index $i$: $$f_i^{-1}(\text{inl } 0) = i$$

For any natural number $n$ and any two distinct elements $i, j \in \text{Fin}(n+2)$, let $f_i : \text{Fin}(n+2) \simeq \text{Fin}(1) \oplus \text{Fin}(n+1)$ be the equivalence (bijection) that extracts the $i$-th component. Then the image of $j$ under this equivalence is the inclusion into the right summand of the relative predecessor of $j$ with respect to $i$: $$f_i(j) = \text{inr}(\text{predAboveI}_i(j))$$ where $\text{predAboveI}_i(j)$ is the function that returns $j$ if $j < i$ and $j - 1$ if $j > i$.

For natural numbers $n$ and $m$, given a fixed index $i \in \text{Fin}(n+2)$ and a bijection (equivalence) $\sigma : \text{Fin}(n+2) \xrightarrow{\sim} \text{Fin}(m+2)$, this function defines a map from $\text{Fin}(n+1)$ to $\text{Fin}(m+1)$. For an input $x \in \text{Fin}(n+1)$, the function identifies $x$ with the unique element $j \in \text{Fin}(n+2)$ such that $j \neq i$ via the inverse of `finExtractOne`. It then applies the bijection to obtain $\sigma(j)$ and uses `predAboveI` to re-index $\sigma(j)$ into the set $\text{Fin}(m+1)$ by skipping the value $\sigma(i)$. Effectively, this is the map between the remaining finite sets obtained by removing $i$ from the domain and $\sigma(i)$ from the codomain.

Let $n, m$ be natural numbers. For any index $i \in \text{Fin}(n+2)$ and any bijection $\sigma : \text{Fin}(n+2) \simeq \text{Fin}(m+2)$, let $f_{i, \sigma} : \text{Fin}(n+1) \to \text{Fin}(m+1)$ be the induced map obtained by removing $i$ from the domain and $\sigma(i)$ from the codomain. Then the composition of $f_{i, \sigma}$ with the map induced by the inverse bijection $\sigma^{-1}$ (relative to the pivot $\sigma(i)$) is the identity on $\text{Fin}(n+1)$: $$(f_{\sigma(i), \sigma^{-1}} \circ f_{i, \sigma}) = \text{id}_{\text{Fin}(n+1)}$$ where $f_{\sigma(i), \sigma^{-1}} : \text{Fin}(m+1) \to \text{Fin}(n+1)$ is the map obtained by removing $\sigma(i)$ from the domain of $\sigma^{-1}$ and $i$ from its codomain.

For natural numbers $n, m \in \mathbb{N}$, given an index $i \in \text{Fin}(n+2)$ and a bijection (equivalence) $\sigma : \text{Fin}(n+2) \xrightarrow{\sim} \text{Fin}(m+2)$, this function defines the induced bijection between the reduced sets $\text{Fin}(n+1)$ and $\text{Fin}(m+1)$. It is constructed by removing the element $i$ from the domain and its image $\sigma(i)$ from the codomain. For any $x \in \text{Fin}(n+1)$, the map identifies $x$ with the unique $j \in \text{Fin}(n+2)$ such that $j \neq i$ (using the re-indexing map that skips $i$), applies $\sigma$ to obtain $\sigma(j)$, and then re-indexes $\sigma(j)$ into $\text{Fin}(m+1)$ by skipping the value $\sigma(i)$.

For natural numbers $n$ and $m$, let $e : \text{Fin}(n+2) \simeq \text{Fin}(m+2)$ be a bijection and let $i \in \text{Fin}(n+2)$ be a fixed index. Then the following identity holds: $$e \circ i.\text{succAbove} = (e(i)).\text{succAbove} \circ \text{finExtractOnePerm}_i(e)$$ where $i.\text{succAbove} : \text{Fin}(n+1) \to \text{Fin}(n+2)$ is the map that embeds $\text{Fin}(n+1)$ into $\text{Fin}(n+2)$ by skipping the index $i$, and $\text{finExtractOnePerm}_i(e) : \text{Fin}(n+1) \simeq \text{Fin}(m+1)$ is the induced bijection obtained by removing $i$ from the domain and $e(i)$ from the codomain of $e$.

For any natural number $n$, let $\sigma : \text{Fin}(n+2) \simeq \text{Fin}(n+2)$ be a bijection and let $i \in \text{Fin}(n+2)$ be a fixed index. The value of the induced bijection $\text{finExtractOnePerm}_i(\sigma) : \text{Fin}(n+1) \simeq \text{Fin}(n+1)$ (obtained by removing $i$ from the domain and $\sigma(i)$ from the codomain) at any $x \in \text{Fin}(n+1)$ is given by the formula: $$\text{finExtractOnePerm}_i(\sigma)(x) = \text{predAbove}_{\sigma(i)}(\sigma(i.\text{succAbove}(x)))$$ where: - $i.\text{succAbove} : \text{Fin}(n+1) \to \text{Fin}(n+2)$ is the map that embeds $\text{Fin}(n+1)$ into $\text{Fin}(n+2)$ by skipping the index $i$. - $\text{predAbove}_{\sigma(i)} : \text{Fin}(n+2) \to \text{Fin}(n+1)$ is the function that maps $y \in \text{Fin}(n+2)$ to $y$ if $y < \sigma(i)$ and to $y-1$ if $y > \sigma(i)$.

For any natural number $n$, let $\sigma : \text{Fin}(n+2) \simeq \text{Fin}(n+2)$ be a bijection and $i \in \text{Fin}(n+2)$ be a fixed index. Let $\tau = \text{finExtractOnePerm}_i(\sigma) : \text{Fin}(n+1) \simeq \text{Fin}(n+1)$ be the induced bijection obtained by removing the element $i$ from the domain and its image $\sigma(i)$ from the codomain. For any $x \in \text{Fin}(n+1)$, the value of the inverse bijection $\tau^{-1}(x)$ is given by: $$\tau^{-1}(x) = \text{predAbove}_{i}(\sigma^{-1}(\sigma(i).\text{succAbove}(x)))$$ where: - $\sigma(i).\text{succAbove} : \text{Fin}(n+1) \to \text{Fin}(n+2)$ is the map that embeds $\text{Fin}(n+1)$ into $\text{Fin}(n+2)$ by skipping the index $\sigma(i)$. - $\text{predAbove}_{i} : \text{Fin}(n+2) \to \text{Fin}(n+1)$ is the function that maps $y \in \text{Fin}(n+2)$ to $y$ if $y < i$ and to $y-1$ if $y > i$. - $\sigma^{-1}$ is the inverse bijection of $\sigma$.

For any natural number $n$, given indices $i \in \text{Fin}(n+2)$ and $j \in \text{Fin}(n+1)$, this definition provides an equivalence (a bijection) between the finite set $\text{Fin}(n+2) = \{0, 1, \dots, n+1\}$ and the iterated disjoint union $(\text{Fin}(1) \oplus \text{Fin}(1)) \oplus \text{Fin}(n)$. The mapping is constructed such that: 1. The element $i$ is mapped to the first summand $\text{Fin}(1)$. 2. The element $i.\text{succAbove}(j)$ (the $j$-th element of $\text{Fin}(n+2)$ when $i$ is excluded) is mapped to the second summand $\text{Fin}(1)$. 3. The remaining $n$ elements of $\text{Fin}(n+2)$ are mapped bijectively to the summand $\text{Fin}(n)$.

For any natural number $n$, an index $i \in \text{Fin}(n+2)$, and an index $j \in \text{Fin}(n+1)$, let $f_{i,j} : \text{Fin}(n+2) \simeq (\text{Fin}(1) \oplus \text{Fin}(1)) \oplus \text{Fin}(n)$ be the equivalence defined by `finExtractTwo i j` (which maps $i$ and the $j$-th element of the remaining set to the two $\text{Fin}(1)$ summands). Then the image of $i$ under this equivalence is $\text{inl}(\text{inl}(0))$, representing the unique element in the first $\text{Fin}(1)$ summand.

For any natural number $n$, let $i \in \text{Fin}(n+2)$ and $j \in \text{Fin}(n+1)$. Let $e : \text{Fin}(n+2) \simeq (\text{Fin}(1) \oplus \text{Fin}(1)) \oplus \text{Fin}(n)$ be the equivalence (bijection) defined by `finExtractTwo i j`, which extracts the index $i$ and the index $i.\text{succAbove}(j)$. The composition of the inverse equivalence $e^{-1}$ with the inclusion of the third summand $\text{inr} : \text{Fin}(n) \to (\text{Fin}(1) \oplus \text{Fin}(1)) \oplus \text{Fin}(n)$ is given by the composition of two skip-index functions: $$e^{-1} \circ \text{inr} = i.\text{succAbove} \circ j.\text{succAbove}$$ where $k.\text{succAbove} : \text{Fin}(m) \to \text{Fin}(m+1)$ is the function that embeds $\text{Fin}(m)$ into $\text{Fin}(m+1)$ by skipping the index $k$.

For any natural number $n$, index $i \in \text{Fin}(n+2)$, index $j \in \text{Fin}(n+1)$, and element $x \in \text{Fin}(n)$, let $e: \text{Fin}(n+2) \simeq (\text{Fin}(1) \oplus \text{Fin}(1)) \oplus \text{Fin}(n)$ be the equivalence (bijection) defined by `finExtractTwo i j`, which extracts the indices $i$ and $i.\text{succAbove}(j)$. The inverse equivalence $e^{-1}$ maps an element $x$ from the third summand $\text{Fin}(n)$ back to $\text{Fin}(n+2)$ according to the formula: $$e^{-1}(\text{inr } x) = i.\text{succAbove}(j.\text{succAbove}(x))$$ where $k.\text{succAbove} : \text{Fin}(m) \to \text{Fin}(m+1)$ is the function that embeds $\text{Fin}(m)$ into $\text{Fin}(m+1)$ by skipping the index $k$, and $\text{inr}$ denotes the inclusion into the right summand of the disjoint union.

For any natural number $n$, index $i \in \text{Fin}(n+2)$, and index $j \in \text{Fin}(n+1)$, let $e: \text{Fin}(n+2) \simeq (\text{Fin}(1) \oplus \text{Fin}(1)) \oplus \text{Fin}(n)$ be the equivalence (bijection) defined by `finExtractTwo i j`, which extracts the indices $i$ and $i.\text{succAbove}(j)$. Then the inverse equivalence $e^{-1}$ maps the unique element in the second $\text{Fin}(1)$ summand to $i.\text{succAbove}(j)$. Specifically, $$e^{-1}(\text{inl}(\text{inr } 0)) = i.\text{succAbove}(j)$$ where $\text{inl}(\text{inr } 0)$ represents the unique element of the second summand in the disjoint union and $i.\text{succAbove} : \text{Fin}(n+1) \to \text{Fin}(n+2)$ is the function that embeds $\text{Fin}(n+1)$ into $\text{Fin}(n+2)$ by skipping the index $i$.

For any natural number $n$, index $i \in \text{Fin}(n+2)$, and index $j \in \text{Fin}(n+1)$, let $e: \text{Fin}(n+2) \simeq (\text{Fin}(1) \oplus \text{Fin}(1)) \oplus \text{Fin}(n)$ be the equivalence (bijection) defined by `finExtractTwo i j`. Then the inverse equivalence $e^{-1}$ maps the element in the first $\text{Fin}(1)$ summand to $i$. Specifically, $e^{-1}(\text{inl}(\text{inl}(0))) = i$, where $\text{inl}(\text{inl}(0))$ represents the unique element of the first summand of the disjoint union.

For any natural number $n$, index $i \in \text{Fin}(n+2)$, and index $j \in \text{Fin}(n+1)$, let $e: \text{Fin}(n+2) \simeq (\text{Fin}(1) \oplus \text{Fin}(1)) \oplus \text{Fin}(n)$ be the equivalence defined by `finExtractTwo i j`. Then applying $e$ to the element $i.\text{succAbove}(j)$ yields $\text{inl}(\text{inr } 0)$, which represents the unique element of the second $\text{Fin}(1)$ summand in the disjoint union.

Let $n, m$ be natural numbers. Suppose $f_1 : \text{Fin}(n) \to \text{Fin}(m)$ and $f_2 : \text{Fin}(m) \to \text{Fin}(n)$ are functions such that $f_1$ and $f_2$ are inverses of each other (i.e., $f_1(f_2(y)) = y$ for all $y \in \text{Fin}(m)$ and $f_2(f_1(x)) = x$ for all $x \in \text{Fin}(n)$). Let $e$ be the equivalence between $\text{Fin}(n)$ and $\text{Fin}(m)$ constructed from these maps. Then for any $x \in \text{Fin}(n)$, the value of $e(x)$ is equal to $f_1(x)$.

Let $n, m$ be natural numbers. Suppose $f_1: \text{Fin}(n) \to \text{Fin}(m)$ and $f_2: \text{Fin}(m) \to \text{Fin}(n)$ are functions such that $f_1(f_2(x)) = x$ for all $x \in \text{Fin}(m)$ and $f_2(f_1(x)) = x$ for all $x \in \text{Fin}(n)$. Let $e$ be the equivalence (bijection) between $\text{Fin}(n)$ and $\text{Fin}(m)$ constructed from these functions. Then, for any $x \in \text{Fin}(m)$, the inverse of the equivalence applied to $x$ is equal to $f_2(x)$. (Here, $\text{Fin}(k)$ denotes the set of natural numbers $\{0, 1, \dots, k-1\}$).

Let $n, m \in \mathbb{N}$. Suppose we have functions $f_1: \text{Fin}(n) \to \text{Fin}(m)$ and $f_2: \text{Fin}(m) \to \text{Fin}(n)$ such that $f_1$ and $f_2$ are inverses of each other, i.e., $f_1(f_2(x)) = x$ for all $x \in \text{Fin}(m)$ and $f_2(f_1(x)) = x$ for all $x \in \text{Fin}(n)$. Then the inverse (symmetry) of the equivalence $\text{finMapToEquiv}(f_1, f_2, h, h')$ constructed from these functions is equal to the equivalence $\text{finMapToEquiv}(f_2, f_1, h', h)$ constructed by swapping the roles of $f_1$ and $f_2$.

Given an equivalence $e : \text{Fin}(n) \simeq \text{Fin}(m)$ between the sets of natural numbers $\{0, \dots, n-1\}$ and $\{0, \dots, m-1\}$, this definition constructs an induced equivalence $e' : \text{Fin}(n+1) \simeq \text{Fin}(m+1)$. The mapping $e'$ is defined such that $e'(0) = 0$, and for any $i \in \{0, \dots, n-1\}$, $e'(i+1) = e(i) + 1$. Its inverse is defined analogously using the inverse of $e$.

Let $n$ and $m$ be natural numbers and let $e : \text{Fin}(n) \simeq \text{Fin}(m)$ be an equivalence between the sets $\{0, \dots, n-1\}$ and $\{0, \dots, m-1\}$. Let $\text{equivCons}(e) : \text{Fin}(n+1) \simeq \text{Fin}(m+1)$ be the extended equivalence. Then the image of $0$ under $\text{equivCons}(e)$ is $0$.

For any natural numbers $n, m, k$ and any equivalences $e : \text{Fin}(n) \simeq \text{Fin}(m)$ and $f : \text{Fin}(m) \simeq \text{Fin}(k)$, the extension of their composition to $\text{Fin}(n+1) \simeq \text{Fin}(k+1)$ via `equivCons` is equal to the composition of their individual extensions. That is, $\text{equivCons}(f \circ e) = \text{equivCons}(f) \circ \text{equivCons}(e)$.

For any natural numbers $n$ and $m$ such that $n = m$, let $e : \text{Fin}(n) \simeq \text{Fin}(m)$ be the canonical order-preserving equivalence (cast) between the sets of natural numbers $\text{Fin}(n) = \{0, \dots, n-1\}$ and $\text{Fin}(m) = \{0, \dots, m-1\}$. Then the extension of this equivalence to the successor sets, $\text{equivCons}(e) : \text{Fin}(n+1) \simeq \text{Fin}(m+1)$—defined by mapping $0$ to $0$ and $i+1$ to $e(i)+1$—is equal to the canonical order-preserving equivalence between $\text{Fin}(n+1)$ and $\text{Fin}(m+1)$.

Let $n$ and $m$ be natural numbers and let $e : \text{Fin } n \simeq \text{Fin } m$ be an equivalence between the sets of natural numbers $\{0, \dots, n-1\}$ and $\{0, \dots, m-1\}$. Let $E : \text{Fin}(n+1) \simeq \text{Fin}(m+1)$ be the induced equivalence (defined as `equivCons e`) such that $E(0) = 0$ and $E(j+1) = e(j) + 1$ for all $j < n$. Then for any $i < m$, the inverse of this extended equivalence satisfies $E^{-1}(i+1) = e^{-1}(i) + 1$.

Let $n, m \in \mathbb{N}$ and let $e: \text{Fin}(n) \simeq \text{Fin}(m)$ be an equivalence between the sets $\{0, \dots, n-1\}$ and $\{0, \dots, m-1\}$. Let $e': \text{Fin}(n+1) \simeq \text{Fin}(m+1)$ be the extended equivalence constructed by `Fin.equivCons`, which maps $0$ to $0$ and increments the image of all other elements by $1$. For any natural number $i$ such that $i+1 < n+1$, the value of $e'$ at $i+1$ is given by $e'(i+1) = e(i) + 1$.