Physlib.Relativity.Tensors.Contraction.SuccSuccAbove

Given two indices $i, j \in \text{Fin}(n+2)$, the function $\text{succSuccAbove}_{i,j}$ maps an element $m \in \text{Fin}(n)$ to an element in $\text{Fin}(n+2)$ by skipping the indices $i$ and $j$. The mapping is defined piecewise as follows: - It returns $m$ if $m < i$ and $m < j$. - It returns $m+1$ if $m+1 < i$ and $j \leq m$. - It returns $m+1$ if $i \leq m$ and $m+1 < j$. - It returns $m+2$ otherwise. This function acts as an order-preserving embedding from $\text{Fin}(n)$ to $\text{Fin}(n+2)$ that omits the values $i$ and $j$.

For any $n \in \mathbb{N}$, given indices $i, j \in \text{Fin}(n+2)$ and an element $m \in \text{Fin}(n)$, the numerical value of the embedding $\text{succSuccAbove}_{i,j}(m)$ is given by the following piecewise definition: $$\text{val}(\text{succSuccAbove}_{i,j}(m)) = \begin{cases} m & \text{if } m < i \text{ and } m < j \\ m + 1 & \text{if } m + 1 < i \text{ and } j \leq m \\ m + 1 & \text{if } i \leq m \text{ and } m + 1 < j \\ m + 2 & \text{otherwise} \end{cases}$$ where all variables are treated as their corresponding natural numbers in the inequalities and arithmetic operations.

For any $n \in \mathbb{N}$, given an index $i \in \text{Fin}(n+2)$ and an element $m \in \text{Fin}(n)$, the value of the order-preserving embedding $\text{succSuccAbove}_{i,i}(m)$ is given by the following piecewise definition: $$\text{succSuccAbove}_{i,i}(m) = \begin{cases} m & \text{if } m < i \\ m + 2 & \text{if } m \geq i \end{cases}$$ where the comparison and addition are performed on the underlying natural values of the finite set elements.

For any $n \in \mathbb{N}$, given indices $i \in \text{Fin}(n+2)$ and $j \in \text{Fin}(n+1)$, the following identity holds: $$\text{succSuccAbove}_{i, \text{succAbove}_i(j)} = \text{succAbove}_i \circ \text{succAbove}_j$$ where $\text{succAbove}_k$ is the order-preserving embedding that skips index $k$, and $\text{succSuccAbove}_{a, b}$ is the order-preserving embedding from $\text{Fin}(n)$ to $\text{Fin}(n+2)$ that skips indices $a$ and $b$.

For any natural number $n$ and any two distinct indices $i, j \in \text{Fin}(n+2)$, the function $\text{succSuccAbove}_{i,j} : \text{Fin}(n) \to \text{Fin}(n+2)$, which is the order-preserving embedding that skips the indices $i$ and $j$, is equal to the composition of two $\text{succAbove}$ mappings: $$\text{succSuccAbove}_{i,j} = \text{succAbove}_i \circ \text{succAbove}_{k}$$ where the index $k \in \text{Fin}(n+1)$ is given by $k = \text{predAbove}_{p}(j)$ with $p = \text{predAbove}_0(i)$. Here, $\text{succAbove}_i$ denotes the order-preserving embedding that skips index $i$, and $\text{predAbove}_p$ is the function that maps $\text{Fin}(m+1)$ to $\text{Fin}(m)$ by collapsing the index $p$.

For any natural number $n$ and any indices $i, j \in \text{Fin}(n+2)$, the function $\text{succSuccAbove}_{i,j} : \text{Fin}(n) \to \text{Fin}(n+2)$ is injective.

Let $n$ be a natural number and let $i, j$ be indices in $\text{Fin}(n+2)$. The function $\text{succSuccAbove}_{i,j} : \text{Fin}(n) \to \text{Fin}(n+2)$ is an embedding that skips the values $i$ and $j$. For any $m_1, m_2 \in \text{Fin}(n)$, it holds that $\text{succSuccAbove}_{i,j}(m_1) = \text{succSuccAbove}_{i,j}(m_2)$ if and only if $m_1 = m_2$.

Let $n$ be a natural number and let $i, j$ be indices in $\text{Fin}(n+2)$. The function $\text{succSuccAbove}_{i,j} : \text{Fin}(n) \to \text{Fin}(n+2)$ is an order-preserving embedding that skips the values $i$ and $j$. For any $m_1, m_2 \in \text{Fin}(n)$, it holds that $\text{succSuccAbove}_{i,j}(m_1) \le \text{succSuccAbove}_{i,j}(m_2)$ if and only if $m_1 \le m_2$.

Let $n$ be a natural number and let $i, j$ be indices in $\text{Fin}(n+2)$. The function $\text{succSuccAbove}_{i,j} : \text{Fin}(n) \to \text{Fin}(n+2)$ is an order-preserving embedding that skips the values $i$ and $j$. For any $m_1, m_2 \in \text{Fin}(n)$, it holds that $\text{succSuccAbove}_{i,j}(m_1) < \text{succSuccAbove}_{i,j}(m_2)$ if and only if $m_1 < m_2$.

Let $n$ be a natural number and let $i, j \in \text{Fin}(n+2)$ be two indices. The function $\text{succSuccAbove}_{i,j} : \text{Fin}(n) \to \text{Fin}(n+2)$, which embeds $\text{Fin}(n)$ into $\text{Fin}(n+2)$ by skipping the indices $i$ and $j$, is monotone. That is, for any $m_1, m_2 \in \text{Fin}(n)$, if $m_1 \leq m_2$, then $\text{succSuccAbove}_{i,j}(m_1) \leq \text{succSuccAbove}_{i,j}(m_2)$.

Let $n$ be a natural number. For any indices $i, j \in \text{Fin}(n+2)$, the function $\text{succSuccAbove}_{i,j} : \text{Fin}(n) \to \text{Fin}(n+2)$, which maps an element $m$ to an element in $\text{Fin}(n+2)$ by skipping the values $i$ and $j$, is strictly monotone.

For any natural number $n$ and any two distinct indices $i, j \in \text{Fin}(n+2)$, the range of the function $\text{succSuccAbove}_{i,j} : \text{Fin}(n) \to \text{Fin}(n+2)$ is the complement of the set $\{i, j\}$. In other words, the image of the mapping consists of all elements in $\text{Fin}(n+2)$ except for $i$ and $j$.

For any natural number $n$ and any two distinct indices $i, j \in \text{Fin}(n+2)$, the function $\text{succSuccAbove}_{i,j} : \text{Fin}(n) \to \text{Fin}(n+2)$ is equal to the unique order-preserving embedding from $\text{Fin}(n)$ to the complement of $\{i, j\}$ in $\text{Fin}(n+2)$.

For any natural number $n$ and indices $i, j \in \text{Fin}(n+2)$, the function $\text{succSuccAbove}_{i,j} : \text{Fin}(n) \to \text{Fin}(n+2)$, which provides an order-preserving embedding skipping the indices $i$ and $j$, is symmetric with respect to those indices. That is, $\text{succSuccAbove}_{i,j} = \text{succSuccAbove}_{j,i}$.

Let $n$ be a natural number and $C$ be a type. For any function $c : \text{Fin}(n+2) \to C$, any indices $i, j \in \text{Fin}(n+2)$, and any $k \in \text{Fin}(n)$, it holds that $$c(\text{succSuccAbove}_{i,j}(k)) = c(\text{succSuccAbove}_{j,i}(k)),$$ where $\text{succSuccAbove}_{i,j}$ is the order-preserving embedding from $\text{Fin}(n)$ to $\text{Fin}(n+2)$ that skips the indices $i$ and $j$.

Let $n$ be a natural number and let $i, j \in \text{Fin}(n+2)$ be distinct indices ($i \neq j$). Let $\text{succSuccAbove}_{i,j} : \text{Fin}(n) \to \text{Fin}(n+2)$ be the order-preserving embedding that omits the values $i$ and $j$. Then, for any $m \in \text{Fin}(n)$, the value $(\text{succSuccAbove}_{i,j})\, m$ is equal to the image of $m$ under the unique order isomorphism from $\text{Fin}(n)$ to the complement set $\{i, j\}^c \subset \text{Fin}(n+2)$.

Let $n$ be a natural number and $i, j \in \text{Fin}(n+2)$ be two distinct indices ($i \neq j$). Let $\text{succSuccAbove}_{i,j} : \text{Fin}(n) \to \text{Fin}(n+2)$ be the order-preserving embedding that omits the values $i$ and $j$. For any subset $X \subseteq \text{Fin}(n)$, the image of the complement $X^c$ under this embedding is equal to the complement of the set $\{i, j\} \cup \text{succSuccAbove}_{i,j}(X)$ in $\text{Fin}(n+2)$. That is, $$\text{succSuccAbove}_{i,j}(X^c) = (\{i, j\} \cup \text{succSuccAbove}_{i,j}(X))^c.$$

For any natural number $n$, let $i, j \in \text{Fin}(n+2)$ be indices and $m \in \text{Fin}(n)$ be an element. Let $\text{succSuccAbove}_{i,j} : \text{Fin}(n) \to \text{Fin}(n+2)$ be the order-preserving embedding that omits the values $i$ and $j$. Then the index $i$ is not equal to the image of $m$ under this mapping, that is, $i \neq \text{succSuccAbove}_{i,j}(m)$.

For any natural number $n$ and any indices $i, j \in \text{Fin}(n+2)$, let $\text{succSuccAbove}_{i,j} : \text{Fin}(n) \to \text{Fin}(n+2)$ be the order-preserving embedding that skips the indices $i$ and $j$. Then for any $m \in \text{Fin}(n)$, the image $\text{succSuccAbove}_{i,j}(m)$ is never equal to $i$.

For any natural number $n$, let $i, j \in \text{Fin}(n+2)$ be two indices and $m \in \text{Fin}(n)$ be an element. Then the value of the order-preserving embedding $\text{succSuccAbove}_{i,j}(m)$, which maps $\text{Fin}(n)$ into $\text{Fin}(n+2)$ by skipping indices $i$ and $j$, is not equal to $j$.

For any natural number $n$, let $i, j \in \text{Fin}(n+2)$ and $m \in \text{Fin}(n)$. The function $\text{succSuccAbove}_{i,j}(m)$, which defines an order-preserving embedding from $\text{Fin}(n)$ to $\text{Fin}(n+2)$ by skipping the indices $i$ and $j$, satisfies $\text{succSuccAbove}_{i,j}(m) \neq j$.

For any natural number $n$, indices $i, j \in \text{Fin}(n+2)$, and $m \in \text{Fin}(n)$, if $m < i$ and $m < j$, then the embedding $\text{succSuccAbove}_{i,j}(m)$ is equal to $m$ (viewed as an element of $\text{Fin}(n+2)$).

For any natural numbers $n$ and $n_1$, given indices $i, j \in \text{Fin}(n+2)$ and $m \in \text{Fin}(n_1)$, let $i'$ and $j'$ be the indices in $\text{Fin}(n_1 + n + 2)$ obtained by shifting $i$ and $j$ by $n_1$ (i.e., $i' = i + n_1$ and $j' = j + n_1$). The order-preserving embedding $\text{succSuccAbove}_{i', j'}$ maps the index $m \in \text{Fin}(n_1)$ to itself in $\text{Fin}(n_1 + n + 2)$.

For any natural numbers $n$ and $n_1$, and indices $i, j \in \text{Fin}(n+2)$, let $i' = n_1 + i$ and $j' = n_1 + j$ be indices in $\text{Fin}(n_1 + n + 2)$ obtained via `Fin.natAdd`. The image of the range of the embedding $\text{castAdd} : \text{Fin}(n_1) \to \text{Fin}(n_1 + n)$ under the skip-embedding $\text{succSuccAbove}_{i', j'}$ is the set of elements in $\text{Fin}(n_1 + n + 2)$ whose value is strictly less than $n_1$, i.e., $\{k \in \text{Fin}(n_1 + n + 2) \mid k < n_1\}$.

For any natural numbers $n$ and $n_1$, given indices $i, j \in \text{Fin}(n+2)$ and $m \in \text{Fin}(n)$, the order-preserving embedding $\text{succSuccAbove}$ satisfies the following translation property: $$\text{succSuccAbove}_{n_1+i, n_1+j}(n_1+m) = n_1 + \text{succSuccAbove}_{i, j}(m)$$ where $n_1 + x$ denotes the index $x$ shifted by $n_1$ (formally defined as `Fin.natAdd n1 x`).

For a natural number $n$, let $i, j \in \text{Fin}(n+2)$ be two distinct indices and $m \in \text{Fin}(n+2)$ be an element such that $m \neq i$ and $m \neq j$. The function `predPredAbove` returns the unique element $k \in \text{Fin } n$ such that $\text{succSuccAbove}(i, j, k) = m$. This corresponds to the preimage of $m$ under the embedding that skips indices $i$ and $j$. The value is calculated by subtracting from $m$ the number of indices in $\{i, j\}$ that are strictly less than $m$: $$\text{predPredAbove}(i, j, m) = m - \mathbb{1}_{i < m} - \mathbb{1}_{j < m}$$ where $\mathbb{1}$ is the indicator function.

For a natural number $n$, let $i, j, m \in \text{Fin}(n+2)$ be indices such that $i \neq j$ and $m$ is distinct from both $i$ and $j$. The natural number value (numerical value) of $\text{predPredAbove}(i, j, m) \in \text{Fin } n$ is given by: - $m$, if $m < i$ and $m < j$; - $m - 1$, if $i < m < j$ or $j < m < i$; - $m - 2$, if $i < m$ and $j < m$. This can be written more formally as: $$\text{val}(\text{predPredAbove}(i, j, m)) = \begin{cases} m & \text{if } m < i \text{ and } m < j \\ m - 1 & \text{if } (i < m < j) \text{ or } (j < m < i) \\ m - 2 & \text{if } m > i \text{ and } m > j \end{cases}$$

For a natural number $n$, let $i, j \in \text{Fin}(n+2)$ be two distinct indices ($i \neq j$) and let $m \in \text{Fin}(n+2)$ be an element such that $m \neq i$ and $m \neq j$. Then the order-preserving embedding $\text{succSuccAbove}_{i,j} : \text{Fin } n \to \text{Fin}(n+2)$, which skips the indices $i$ and $j$, and the function $\text{predPredAbove}_{i,j}$, which maps elements in the complement of $\{i, j\}$ back to $\text{Fin } n$, satisfy the identity: $$\text{succSuccAbove}_{i,j}(\text{predPredAbove}_{i,j}(m)) = m$$

For a natural number $n$, let $i, j \in \text{Fin}(n+2)$ be two distinct indices ($i \neq j$) and let $S = \{i, j\}^c$ be the complement of $\{i, j\}$ in $\text{Fin}(n+2)$. Let $\phi: \text{Fin } n \to S$ be the unique order-preserving isomorphism between $\text{Fin } n$ and the subset $S$. For any $m \in \text{Fin}(n+2)$ such that $m \neq i$ and $m \neq j$, the function $\text{predPredAbove}$ satisfies: $$\text{predPredAbove}(i, j, m) = \phi^{-1}(m)$$

Let $n$ be a natural number and let $i, j \in \text{Fin}(n+2)$ be two distinct indices ($i \neq j$). For any elements $m_1, m_2 \in \text{Fin}(n+2)$ such that $m_1 \notin \{i, j\}$ and $m_2 \notin \{i, j\}$, the function $\text{predPredAbove}$ is injective, meaning: $$\text{predPredAbove}(i, j, m_1) = \text{predPredAbove}(i, j, m_2) \iff m_1 = m_2$$

Let $n$ be a natural number and let $i, j \in \text{Fin}(n+2)$ be distinct indices ($i \neq j$). For every $m \in \text{Fin } n$, there exists an element $m' \in \text{Fin}(n+2)$ such that $m' \neq i$ and $m' \neq j$, which satisfies $\text{predPredAbove}(i, j, m') = m$.

For any natural number $n$, let $i, j \in \text{Fin}(n+2)$ be two distinct indices ($i \neq j$) and let $m \in \text{Fin } n$. Then applying the function $\text{predPredAbove}_{i, j}$ to the result of the embedding $\text{succSuccAbove}_{i, j}(m)$ returns the original value $m$: $$\text{predPredAbove}(i, j, \text{succSuccAbove}(i, j, m)) = m$$ where $\text{succSuccAbove}(i, j, \cdot)$ is the order-preserving embedding from $\text{Fin}(n)$ to $\text{Fin}(n+2)$ that skips indices $i$ and $j$, and $\text{predPredAbove}(i, j, \cdot)$ is the map that collapses $\text{Fin}(n+2) \setminus \{i, j\}$ back to $\text{Fin } n$.

For any natural number $n$, let $i_1, j_1 \in \text{Fin}(n+4)$ be two distinct indices and $i_2, j_2 \in \text{Fin}(n+2)$ be two distinct indices. Define the transformed indices in $\text{Fin}(n+4)$ as $i_2' = \text{succSuccAbove}(i_1, j_1, i_2)$ and $j_2' = \text{succSuccAbove}(i_1, j_1, j_2)$, and the transformed indices in $\text{Fin}(n+2)$ as $i_1' = \text{predPredAbove}(i_2', j_2', i_1)$ and $j_1' = \text{predPredAbove}(i_2', j_2', j_1)$. Then the following equality of compositions of embeddings holds: $$\text{succSuccAbove}(i_1, j_1) \circ \text{succSuccAbove}(i_2, j_2) = \text{succSuccAbove}(i_2', j_2') \circ \text{succSuccAbove}(i_1', j_1')$$ where $\text{succSuccAbove}(i, j, \cdot)$ is the order-preserving embedding that maps an element to a larger finite set by skipping the indices $i$ and $j$, and $\text{predPredAbove}(i, j, \cdot)$ is its left inverse mapping elements from the complement of $\{i, j\}$.

Let $n$ be a natural number. Given distinct indices $i_1, j_1 \in \text{Fin}(n+4)$ and distinct indices $i_2, j_2 \in \text{Fin}(n+2)$, we define the following transformed indices: 1. $i_2' = \text{succSuccAbove}(i_1, j_1, i_2)$ and $j_2' = \text{succSuccAbove}(i_1, j_1, j_2)$ as the images of $i_2$ and $j_2$ in $\text{Fin}(n+4)$ under the embedding that skips $i_1$ and $j_1$. 2. $i_1' = \text{predPredAbove}(i_2', j_2', i_1)$ and $j_1' = \text{predPredAbove}(i_2', j_2', j_1)$ as the preimages of $i_1$ and $j_1$ in $\text{Fin}(n+2)$ under the map that "collapses" the holes at $i_2'$ and $j_2'$. For any $m \in \text{Fin}(n)$, the composition of these double-skipping embeddings satisfies the following commutativity relation: $$\text{succSuccAbove}(i_2', j_2', \text{succSuccAbove}(i_1', j_1', m)) = \text{succSuccAbove}(i_1, j_1, \text{succSuccAbove}(i_2, j_2, m))$$ where $\text{succSuccAbove}(i, j, \cdot)$ is the order-preserving embedding that skips indices $i$ and $j$, and $\text{predPredAbove}(i, j, \cdot)$ is its left inverse.

For natural numbers $n$ and $n_1$, given a bijection $\sigma : \text{Fin}(n_1 + 2) \to \text{Fin}(n + 2)$ and two distinct indices $i, j \in \text{Fin}(n_1 + 2)$, the function `funPredPredAbove` defines a map from $\text{Fin}(n_1)$ to $\text{Fin}(n)$. For an element $m \in \text{Fin}(n_1)$, its image is defined by: $$\text{funPredPredAbove}(i, j, \sigma, m) = \text{predPredAbove}(\sigma(i), \sigma(j), \sigma(\text{succSuccAbove}(i, j, m)))$$ where $\text{succSuccAbove}_{i,j}$ is the embedding that skips $i$ and $j$, and $\text{predPredAbove}_{\sigma(i), \sigma(j)}$ is the map that collapses the indices by skipping the images $\sigma(i)$ and $\sigma(j)$. This function represents the bijection between $\text{Fin}(n_1)$ and $\text{Fin}(n)$ induced by $\sigma$ after removing $i$ and $j$ from the domain and their images from the codomain.

Let $n$ and $n_1$ be natural numbers. Given a bijective function $\sigma : \text{Fin}(n_1 + 2) \to \text{Fin}(n + 2)$ and two distinct indices $i, j \in \text{Fin}(n_1 + 2)$, the induced function $\text{funPredPredAbove}_{i,j, \sigma} : \text{Fin}(n_1) \to \text{Fin}(n)$ is injective. This function is defined as: $$\text{funPredPredAbove}(i, j, \sigma, m) = \text{predPredAbove}(\sigma(i), \sigma(j), \sigma(\text{succSuccAbove}(i, j, m)))$$ where $\text{succSuccAbove}_{i,j}$ is the embedding that skips $i$ and $j$, and $\text{predPredAbove}_{\sigma(i), \sigma(j)}$ is the map that collapses the codomain by skipping the images $\sigma(i)$ and $\sigma(j)$.

For natural numbers $n$ and $n_1$, let $\sigma: \text{Fin}(n_1 + 2) \to \text{Fin}(n + 2)$ be a bijective function and $i, j \in \text{Fin}(n_1 + 2)$ be distinct indices. The induced map $\text{funPredPredAbove}(i, j, \sigma, \cdot): \text{Fin}(n_1) \to \text{Fin}(n)$, which is defined by skipping the indices $i, j$ in the domain and their images $\sigma(i), \sigma(j)$ in the codomain, is surjective.

Let $n$ and $n_1$ be natural numbers. Given two distinct indices $i, j \in \text{Fin}(n_1 + 2)$ and a bijective function $\sigma : \text{Fin}(n_1 + 2) \to \text{Fin}(n + 2)$, the induced map $\text{funPredPredAbove}_{i, j, \sigma} : \text{Fin}(n_1) \to \text{Fin}(n)$ is bijective. This map is defined by applying $\sigma$ to an element after skipping indices $i$ and $j$ via $\text{succSuccAbove}$, and then collapsing the resulting indices in the codomain by skipping $\sigma(i)$ and $\sigma(j)$ via $\text{predPredAbove}$.

For any natural number $n_1$ and any two distinct indices $i, j \in \text{Fin}(n_1 + 2)$, the function $\text{funPredPredAbove}$ induced by the identity function $\text{id} : \text{Fin}(n_1 + 2) \to \text{Fin}(n_1 + 2)$ is equal to the identity function on $\text{Fin}(n_1)$.