The Strict Prefix Map on the Observation Record Space

Let $\tilde{l}\ge1$ be a natural number, let $T>0$ be a real number, and let $\mathbf{R}=\mathbf{R}(T,\tilde{l})$ be the observation record space with horizon $T$ and $\tilde{l}$ channels, records written $r=(k,t,v)$ with $t=(t_1,\dots,t_k)$ and $v=(v_1,\dots,v_k)$ as there.

For $s\in[0,T]$ the strict prefix map $\pi_{s-}:\mathbf{R}\to\mathbf{R}$ sends a record $r=(k,t,v)$ to $\pi_{s-}(r)=\bigl(\kappa,\ (t_1,\dots,t_\kappa),\ (v_1,\dots,v_\kappa)\bigr),$ where $\kappa$ is the number of indices $i\in\{1,\dots,k\}$ with $t_i<s$, and both tuples are empty when $\kappa=0$. Since $t_1<\dots<t_k$, the indices with $t_i<s$ are exactly $1,\dots,\kappa$, so $\pi_{s-}(r)$ is again a record with horizon $T$. (This map keeps the events strictly before $s$ and keeps the horizon $T$; it is distinct from the prefix map $\pi_s$ of Splitting of the Observation Record Space at an Intermediate Time, which keeps the events with $t_i\le s$ and has horizon $s$.)