Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices

¶ This setting extends Metric Spaces: Balls, the Metric Topology, and the Real and Complex Numbers as Metric Spaces: its conventions and notation are in force.

¶ Arithmetic and order in $\mathbb{R}$ obey Arithmetic and Order Rules in the Real Numbers, Stated for ℝ. Closure facts in an ordered field are those of Closure Facts in an Ordered Field: Negatives, Differences, Quotients, Absolute Values, Powers, Natural Numbers, Halves and Minima. The sum and the product of complex numbers are binary operations on $\mathbb{C}$, by The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit §operations. Iterated operations and operations over finite sets take values in the underlying set as in Iterated Operations and Operations over Finite Sets Take Values in the Underlying Set.

¶ Values, graphs, restrictions and equality of maps obey Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol. Maps given by iterated operations, powers and operations over a finite set are those of Maps Given by Iterated Operations: Partial Iterates, Images of Natural Numbers, Powers and Operations over a Finite Set, and the distance on $\mathbb{R}$ is a map as in The Distance on the Real Numbers Is a Map with Values the Absolute Differences. The pointwise operations and the constant maps on $\mathbb{R}^{I}$, for a set $I$, exist as in Pointwise Operations on Real-Valued Maps Exist and Are Unique and obey Rules for Pointwise Operations on Real-Valued Maps: a Commutative Ring, Scalar Multiples and Evaluation. Summation over a finite set and, for $n\in\mathbb{N}$, the dot product, the Euclidean norm and the Euclidean distance on $\mathbb{R}^{n}$ are maps as in The Summation Map on Real-Valued Maps over a Finite Set, and the Dot Product, Euclidean Norm and Euclidean Distance as Maps. The matrix product, the matrix-vector product, the transpose and the trace (of square matrices) of real matrices, the identity matrix and the standard basis vectors exist and are unique as in The Matrix Product, Matrix-Vector Product, Transpose, Trace, Identity Matrix and Standard Basis Vectors Exist and Are Unique.

¶ An expression written with abbreviations as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §defined-symbols in which no quantifier is applied to a class variable, counting the quantifiers inside the class abstractions written in it, is predicative, by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §closure; a set that, under a predicative condition, is the only set satisfying a predicative formula may be eliminated through that formula, by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §elimination. Predicative formulas for values of maps and binary operations, for negatives, differences, absolute values, distances, reciprocals and quotients in an ordered field, for iterated operations and operations over finite sets, for limits, suprema and infima, and for maps $u\mapsto t(u)$ given by expressions are those of Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity, Predicative Substitution of Values of Functions and Binary Operations, and Predicative Formulas for Negatives, Differences, Absolute Values, Distances, Reciprocals and Quotients in an Ordered Field, Iterated Operations Are Given by a Predicative Formula, Iterated Operations over Finite Sets Are Given by a Predicative Formula, Predicative Formulas for Convergence and Limits, and Maps Defined by Limits, Predicative Formulas for Suprema and Infima, and Maps Defined by Suprema and Infima and Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol §map-symbol, under their conditions. Classes and maps given by such formulas and expressions are formed as in Sets and Maps: Ordinary Notation §set-builder and Sets and Maps: Ordinary Notation §maps, and maps given by limits, suprema and infima as in Predicative Formulas for Convergence and Limits, and Maps Defined by Limits §maps and Predicative Formulas for Suprema and Infima, and Maps Defined by Suprema and Infima §maps.

¶ Natural numbers used as indices obey Natural Numbers as Indices: ℕ ⊆ ℕ₀, 1 ∈ ℕ₀, and the Two Readings of an Operation from 1 to n: $\mathbb{N}\subseteq\mathbb{N}_{0}$, $1\in\mathbb{N}_{0}$, and for $n\in\mathbb{N}$ both readings of an associative and commutative operation from $1$ to $n$ agree with the operation over $[n]$. Intervals of $\mathbb{N}_{0}$ are as in Intervals of Natural Numbers and obey Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting; finite sets are as in Finite Sets, tuples as in Tuples in a Set: the Set of n-Tuples and Their Components, and properties of relations as in Reflexive, Symmetric, Antisymmetric and Transitive Relations on a Set.

¶ The facts listed in the clauses arithmetic, maps, predicativity and indices, and their elementary consequences, are used without further citation.