Banach indicatrix, easy half: $TV_s^t(F)\le\int i^*_{]s,t]}(h)\,dh$ for càdlàg $F$

Let $F:\mathbb R\to\mathbb R$ be càdlàg (right-continuous with left limits) and let $s\le t$. Write $i^*_{]s,t]}(h)$ for the number of generalized solutions $x\in\,]s,t]$ of $F=h$, i.e. the number of points $x\in\,]s,t]$ with $(x,h)$ in the completed graph of $F$. Then

This is the elementary half of the generalized Banach indicatrix identity, and it holds with no bounded-variation assumption (both sides may be $+\infty$).

The proof is a single application of the generalized intermediate value theorem. For a finite increasing sample $u_0\le\dots\le u_n$ inside $[s,t]$, the $i$-th increment satisfies $|F(u_{i+1})-F(u_i)| = \mathrm{Leb}\big(\,]\min,\max[\,\big)$ where $\min,\max$ are the endpoints of the value interval, so the whole sum equals $\int_{\mathbb R} v(h)\,dh$ with $v(h)$ the number of indices $i$ for which $h$ lies strictly between $F(u_i)$ and $F(u_{i+1})$. Each such index produces, by the generalized intermediate value theorem, a generalized solution inside $]u_i,u_{i+1}]$; these half-open intervals are pairwise disjoint and contained in $]s,t]$, so $v(h)\le i^*_{]s,t]}(h)$ pointwise. Taking the supremum over samples gives the claim.

Formalization note. The total variation is Mathlib's eVariationOn over Icc s t, the count is Set.encard coerced into $[0,\infty]$, and càdlàg is spelled as right continuity within Ici x together with existence of a left limit at every point.