Physlib.Thermodynamics.Temperature.TemperatureUnits

For any temperature unit $x$, its underlying numerical value $x.\text{val}$ is not equal to zero ($x.\text{val} \neq 0$).

For any temperature unit $x$, its underlying numerical value $x.\text{val}$ is strictly greater than zero ($x.\text{val} > 0$).

The type of temperature units, $\text{TemperatureUnit}$, has a default element. This default value is defined as the temperature unit whose underlying positive real value is $1$.

For any two temperature units $x$ and $y$, their division $x / y$ is defined as the ratio of their underlying positive real values, $\frac{x.\text{val}}{y.\text{val}}$, yielding a non-negative real number in $\mathbb{R}_{\ge 0}$.

For any two temperature units $x$ and $y$, the ratio $x/y$ is equal to the quotient of their underlying numerical values $\frac{x.\text{val}}{y.\text{val}}$, considered as a non-negative real number in $\mathbb{R}_{\ge 0}$.

For any two temperature units $x$ and $y$, their ratio $x/y$ is not equal to zero in the set of non-negative real numbers $\mathbb{R}_{\ge 0}$.

For any two temperature units $x$ and $y$, the ratio of their underlying values $x/y$ is strictly greater than zero in the set of non-negative real numbers $\mathbb{R}_{\ge 0}$.

For any temperature unit $x$, the ratio of the unit to itself is equal to one, expressed as $x / x = 1$ in the non-negative real numbers $\mathbb{R}_{\ge 0}$.

For any two temperature units $x$ and $y$, the ratio of $x$ to $y$ is equal to the multiplicative inverse of the ratio of $y$ to $x$. Mathematically, this is expressed as: $$x / y = (y / x)^{-1}$$ where the division $u_1 / u_2$ represents the ratio of the underlying scales of the temperature units as a non-negative real number in $\mathbb{R}_{\ge 0}$.

For any three temperature units $x, y,$ and $z$, the product of the ratio of $x$ to $y$ and the ratio of $y$ to $z$ is equal to the ratio of $x$ to $z$. Expressed as real numbers, this holds as $(x/y) \cdot (y/z) = x/z$, where the division $u_1 / u_2$ represents the ratio of the scales of the temperature units.

For any temperature unit $x$ and any positive real number $r > 0$, the ratio of the temperature unit $x$ scaled by $r$ to the original unit $x$ is equal to $r$. Mathematically, this is expressed as: $$\frac{\text{scale}(r, x)}{x} = r$$ where $\text{scale}(r, x)$ denotes the temperature unit $x$ scaled by the factor $r$, and the division $u_1 / u_2$ represents the ratio of the scales of the temperature units as a non-negative real number.

For any temperature unit $x$ and any positive real number $r > 0$, the ratio of the unit $x$ to the unit $x$ scaled by the factor $r$ is equal to $1/r$. Expressed mathematically: $$x / \text{scale}(r, x) = 1/r$$ In this identity, the division $u_1 / u_2$ represents the ratio of the scales of the temperature units, resulting in a non-negative real number in $\mathbb{R}_{\ge 0}$.

For any temperature unit $x$, scaling $x$ by a factor of $1$ results in the same temperature unit $x$. Mathematically, this is expressed as: $$\text{scale}(1, x) = x$$ where $\text{scale}$ is the operation that scales a given temperature unit by a positive real number.

Let $x_1$ and $x_2$ be two temperature units, and let $r_1, r_2$ be positive real numbers ($r_1 > 0$ and $r_2 > 0$). The ratio of the unit $x_1$ scaled by $r_1$ to the unit $x_2$ scaled by $r_2$ is equal to the ratio of the scaling factors multiplied by the ratio of the original units: $$\frac{\text{scale}(r_1, x_1, hr_1)}{\text{scale}(r_2, x_2, hr_2)} = \frac{r_1}{r_2} \cdot \frac{x_1}{x_2}$$ In this expression, the division of temperature units results in a non-negative real number in $\mathbb{R}_{\ge 0}$ representing the ratio of their underlying values.

For any temperature unit $x$ and any two positive real numbers $r_1, r_2$ (where $r_1 > 0$ and $r_2 > 0$), scaling the unit $x$ first by $r_2$ and then scaling the resulting unit by $r_1$ is equivalent to scaling the original unit $x$ by the product $r_1 \cdot r_2$. This is expressed as: $$\text{scale}(r_1, \text{scale}(r_2, x, hr_2), hr_1) = \text{scale}(r_1 \cdot r_2, x, hr_{1 \cdot 2})$$ where $\text{scale}$ is the operation that scales a temperature unit by a positive factor, and $hr_1, hr_2, hr_{1 \cdot 2}$ are the proofs that the scaling factors are positive.

The temperature unit of Kelvin is defined as the base unit of temperature, corresponding to the value 1 in the representation of `TemperatureUnit` as positive real numbers $\mathbb{R}_{>0}$.

The temperature unit of nanokelvin is defined as the unit obtained by scaling the kelvin unit by a factor of $10^{-9}$.

The temperature unit of $\text{microkelvin}$ is defined as the unit obtained by scaling the $\text{kelvin}$ unit by a factor of $10^{-6}$.

The temperature unit of $\text{millikelvin}$ is defined as the unit obtained by scaling the $\text{kelvin}$ unit by a factor of $10^{-3}$.

The temperature unit $\text{absoluteFahrenheit}$ is defined as the unit obtained by scaling the $\text{kelvin}$ unit by a factor of $\frac{5}{9}$. This represents a temperature scale where the unit magnitude is equal to one degree Fahrenheit, measured from absolute zero.