Cardinality of an Index Interval

This is an elementary cardinality identity for coordinate slots.

For natural numbers $a,b,k$ with $b\le k$, let slots k a b be the positions $p\in\operatorname{Fin}(k)$ satisfying $a\le p<b$. Then

The result is used to verify the sizes of the coordinate blocks in the tensor symmetrization theorem.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis.Tensor. Shown in its original module context. Proof omitted.

theorem card_slots {k a b : ℕ} (hb : b ≤ k) : (slots k a b).card = b - a

Module navigation

Module: Analysis/Tensor/Coordinate.

Next: norm_le_four_pow_mul_norm_symmetrize.

Source excerpt, lines 65–65 · Frozen source 408915f.