UV-compression preserves t-intersecting families

Fix a finite ground set $[n] = \{0, \dots, n-1\}$ and two distinct elements $z, i \in [n]$. Recall the classical shifting (or compression) operation $S_{z,i}$ on subsets of $[n]$: it replaces $i$ by $z$ in any set that contains $i$ but not $z$, and leaves every other set unchanged. Applying $S_{z,i}$ to a family $\mathcal{A}$ produces a new family $S_{z,i}(\mathcal{A})$ of the same cardinality (a set already carrying its own shifted image simply stays put, so nothing is identified or lost).

Let $\mathcal{A}$ be a $t$-intersecting family (TIntersecting): every pair of members $A, B \in \mathcal{A}$, allowing $A = B$, satisfies $|A \cap B| \ge t$. This result shows that shifting preserves this property:

This is the non-uniform generalization of the classical fact, used throughout extremal set theory (starting with the shifting technique in Erdős–Ko–Rado-type arguments), that the shifting operation preserves the (ordinary, $t=1$) intersecting property. Iterating $S_{z,i}$ over all $i \ne z$ therefore lets one replace an arbitrary $t$-intersecting family by one that is compressed toward $z$ without changing its size or its $t$-intersecting property — the key reduction step in Katona's 1964 proof of the maximum size of a $t$-intersecting family.

Formalization note. The shift $S_{z,i}$ is Mathlib's general UV.compress operator specialized to the singletons $\{z\}, \{i\}$, and $S_{z,i}(\mathcal{A})$ is its family-level lift UV.compression (notation 𝓒), already used in Mathlib's proof of the Kruskal–Katona theorem.