Indices which are real numbers (from a finite, ordered set) – name or reference for this

Question

I am trying to improve a rather technical proof. In the old version of the proof, I indexed a finite, ordered sequence of unique positive real numbers $a_1, \dotsc, a_n$. I figured out that using these numbers directly as indices considerably streamlines the notation and further increases readability (as these numbers and not their indices are what matter). For example, instead of

$$ \sum_{\substack{j=1\\a_j<b}}^n a_j \sum_{i∈I_j} c_i, $$

I would now write (with everything being clear in context):

$$ \sum_{a<b} a \sum_{i∈I_a} c_i.$$

The only “problem” is that that I am using a real number as an index in expressions like $I_a$ (and a function notation is not feasible here) and also perform an induction over these numbers. This is maybe a bit of mental gymnastics, but I am confident that it is the lesser evil and mathematically sound.

Now, my question is this: I am probably not the first one to do such a thing.
Is there a name for this notational strategy or something similar that I could use as a reference?
The goal is to provide further reading for the interested or skeptical reader.
It may help that in my context, one can also think of the $a_i$ as equivalence classes.

I found this question and indexed families, but neither satisfies me.

Answer 1

As has been pointed out in a comment, people do this sort of thing all the time. I have only been able to find two texts that can be used as references for the topic. Of the two, the more readable is Terence Tao, Analysis I (1^st edition, Hindustan Book Agency 2006). Here are some extracts:

Definition 7.1.6 (Summations over finite sets). Let $X$ be a finite set with $n$ elements (where $n \in \mathbf{N}$), and let $f \colon X \to \mathbf{R}$ be a function from $X$ to the real numbers (i.e., $f$ assigns a real number $f(x)$ to each element $x$ of $X$). Then we can define the finite sum $\sum_{x \in X} f(x)$ as follows. We first select any bijection $g$ from $\{i \in \mathbf{N} : 1 \leq i \leq n\}$ to $X$; such a bijection exists since $X$ is assumed to have $n$ elements. We then define $$ \sum_{x \in X} f(x) := \sum_{i=1}^n f(g(i)). $$

[$\ldots$]

To verify that this definition actually does give a single, well-defined value to $\sum_{x \in X} f(x),$ one has to check that different bijections $g$ from $\{i \in \mathbf{N} : 1 \leq i \leq n\}$ to $X$ give the same sum. In other words, we must prove

Proposition 7.1.8 (Finite summations are well-defined). Let $X$ be a finite set with $n$ elements (where $n \in \mathbf{N}$), let $f \colon X \to \mathbf{R}$ be a function, and let $g \colon \{i \in \mathbf{N} : 1 \leq i \leq n\} \to X$ and $h \colon \{i \in \mathbf{N} : 1 \leq i \leq n\} \to X$ be bijections. Then we have $$ \sum_{i=1}^n f(g(i)) = \sum_{i=1}^n f(h(i)). $$

The only other useful reference I know of is Nicolas Bourbaki, Elements of Mathematics: Algebra I, Chapters 1–3 (Hermann, Paris 1974, PDF). I’ll only quote one of his results, but the book might be worth exploring further, if it is important to prove things about sums of families defined on finite ordered sets without relying, as Tao does, on the special case where the indices are integers. (I haven’t tried to reproduce Bourbaki’s typography exactly, because I don’t think it’s possible in MathJax, and it would even require some hacking about in LaTeX.)

Theorem 1 (Associativity theorem). Let $E$ be an associative magma whose law is denoted by $\odot.$ Let $A$ be a totally ordered non-empty finite set, which is the union of an ordered sequence of non-empty subsets $(B_i)_{i \in I}$ such that the relations $\alpha \in B_i,$ $\beta \in B_j,$ $i < j$ imply $\alpha < \beta$; let $(x_\alpha)_{\alpha \in A}$ be an ordered sequence of elements of $E$ with $A$ as indexing set. Then $$ \bigodot_{\alpha \in A} x_\alpha = \bigodot_{i \in I}\Big(\bigodot_{\alpha \in B_i} x_\alpha\Big). $$