Set of symbols
Alphabet
Deduction system
Theory
Zermelo-Fraenkel set theory
Set
Binary cartesian set product
Binary relation
Map
Cartesian product
Complex cartesian product
Real cartesian product
Real number collection
Descriptive statistic
Real function arithmetic mean
Formulation 3
Let $[a, b] \subseteq \mathbb{R}$ be a D544: Closed real interval such that
(i) \begin{equation} a < b \end{equation}
(ii) $f : [a, b] \to \mathbb{R}$ is a D1760: Riemann integrable real function
A D993: Real number $a \in \mathbb{R}$ is an arithmetic mean for $f$ if and only if \begin{equation} \int^b_a a \, d t = \int^b_a f(t) \, d t \end{equation}
Child definitions
» D4925: Euclidean real arithmetic mean