Physlib.SpaceAndTime.Time.TimeUnit

For any time unit $x$, its associated real value $x.val$ is not equal to zero.

For any time unit $x$, its underlying real value $x.\text{val}$ is strictly greater than zero, i.e., $x.\text{val} > 0$.

The type of time units, $\text{TimeUnit}$ (representing the set of positive real numbers), is provided with a default inhabitant defined as $1$.

For any two time units $x, t \in \text{TimeUnit}$, their ratio $x / t$ is defined as the quotient of their underlying positive real values $\frac{x_{\text{val}}}{t_{\text{val}}}$, resulting in a non-negative real number in $\mathbb{R}_{\ge 0}$.

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

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

For any two time units $x, y \in \text{TimeUnit}$, their ratio $x / y$ is strictly greater than zero in the non-negative real numbers $\mathbb{R}_{\ge 0}$.

For any time unit $x$, the ratio of $x$ to itself is equal to 1, where the ratio is considered as a non-negative real number ($x / x = 1 \in \mathbb{R}_{\ge 0}$).

For any two time units $x, y \in \text{TimeUnit}$, the ratio $x / y$ is equal to the reciprocal of the ratio $y / x$. That is, $$x / y = (y / x)^{-1}$$ where the division of two time units results in a non-negative real number in $\mathbb{R}_{\ge 0}$.

For any three time units $x, y, z \in \text{TimeUnit}$, 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$. That is, $(x / y) \cdot (y / z) = x / z$, where the ratios are treated as real numbers.

For any time unit $x \in \text{TimeUnit}$ and any positive real number $r > 0$, the ratio of the scaled time unit $\text{scale}(r, x)$ to the original time unit $x$ is equal to $r$. That is, $$\frac{\text{scale}(r, x)}{x} = r$$ where the division of two time units results in a non-negative real number in $\mathbb{R}_{\ge 0}$.

For any time unit $x \in \text{TimeUnit}$, scaling $x$ by a factor of $1$ results in the same time unit $x$. That is, $\text{scale}(1, x) = x$.

For any two time units $x_1$ and $x_2$ and any two positive real numbers $r_1, r_2 > 0$, the ratio of the scaled time units $\text{scale}(r_1, x_1)$ and $\text{scale}(r_2, x_2)$ is equal to the product of the ratio of the scaling factors $\frac{r_1}{r_2}$ and the ratio of the original units $\frac{x_1}{x_2}$: $$\frac{\text{scale}(r_1, x_1)}{\text{scale}(r_2, x_2)} = \frac{r_1}{r_2} \cdot \frac{x_1}{x_2}$$ where the division of two time units results in a non-negative real number.

For any time unit $x \in \text{TimeUnit}$ and any positive real number $r > 0$, the ratio of the original unit $x$ to the unit scaled by $r$ (denoted $\text{scale}(r, x)$) is equal to the reciprocal of the scaling factor, $1/r$. Mathematically, this is expressed as: $$\frac{x}{\text{scale}(r, x)} = \frac{1}{r}$$ where the ratio of two time units is a non-negative real number in $\mathbb{R}_{\ge 0}$.

For any time unit $x \in \text{TimeUnit}$ and any two positive real numbers $r_1, r_2 > 0$, scaling the unit $x$ 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$: $$\text{scale}(r_1, \text{scale}(r_2, x)) = \text{scale}(r_1 \cdot r_2, x)$$ where $\text{scale}(r, x)$ denotes the time unit obtained by scaling $x$ by a factor $r$.

The constant `seconds` is defined as a specific unit of time in the type `TimeUnit`, corresponding to the value $1$ in the set of positive real numbers $\mathbb{R}_{>0}$.

The constant `femtoseconds` is a unit of time defined by scaling the base unit `seconds` by a factor of $10^{-15}$, corresponding to the value of $10^{-15}$ in the set of positive real numbers $\mathbb{R}_{>0}$ representing the time unit.

The constant `picoseconds` is defined as a specific unit of time in the type `TimeUnit`, obtained by scaling the unit `seconds` by a factor of $10^{-12}$.

The constant `nanoseconds` is a unit of time defined as the result of scaling the base unit `seconds` by a factor of $10^{-9}$, corresponding to the value of $10^{-9}$ in the set of positive real numbers $\mathbb{R}_{>0}$ representing the time unit.

The constant `microseconds` is defined as a specific unit of time in the type `TimeUnit`, obtained by scaling the base unit `seconds` by a factor of $10^{-6}$.

The constant `milliseconds` is a unit of time defined as the result of scaling the base unit `seconds` by a factor of $(1/10)^3$, which corresponds to $10^{-3}$ seconds.

The constant `centiseconds` is a unit of time defined as the result of scaling the base unit `seconds` by a factor of $(1/10)^2$, which corresponds to $10^{-2}$ seconds.

The constant `deciseconds` is a unit of time defined as the result of scaling the base unit `seconds` by a factor of $(1/10)^1$, which corresponds to $10^{-1}$ seconds.

The constant `minutes` is a unit of time defined as the result of scaling the base unit `seconds` by a factor of $60$.

The constant `hours` is a unit of time in `TimeUnit` defined as the result of scaling the base unit `seconds` by a factor of $3600$, which represents $60 \times 60$ seconds.

The constant `days` is a unit of time in `TimeUnit` defined as the result of scaling the base unit `seconds` by a factor of $24 \times 60 \times 60 = 86,400$. It represents the duration of a standard 24-hour day.

The time unit $\text{weeks} \in \text{TimeUnit}$ is defined by scaling the unit $\text{seconds}$ by a factor of $7 \times 24 \times 60 \times 60 = 604,800$.

The ratio of the time unit $\text{minutes}$ to the time unit $\text{seconds}$ is equal to the non-negative real number $60$. That is, $$\text{minutes} / \text{seconds} = 60$$ where the division of two time units results in a value in $\mathbb{R}_{\ge 0}$.

The ratio of the time unit of hours to the time unit of seconds is equal to the non-negative real number $3600$. That is, $$\frac{\text{hours}}{\text{seconds}} = 3600$$ where $\text{hours}$ and $\text{seconds}$ are elements of `TimeUnit` and the division operator returns their ratio in $\mathbb{R}_{\ge 0}$.

The ratio of the time unit of days to the time unit of seconds is equal to $86,400$ as a non-negative real number, i.e., $$\text{days} / \text{seconds} = 86,400$$

The ratio of the time unit $\text{weeks}$ to the time unit $\text{seconds}$ is equal to $604,800$. That is, $$\frac{\text{weeks}}{\text{seconds}} = 604,800$$ where the division of these two time units results in a non-negative real number in $\mathbb{R}_{\ge 0}$.

The ratio of the time unit for days to the time unit for minutes is equal to the non-negative real number $1440$, expressed as $\text{days} / \text{minutes} = 1440 \in \mathbb{R}_{\ge 0}$.

The ratio of the time unit $\text{weeks}$ to the time unit $\text{minutes}$ is equal to the non-negative real number $10080$: $$\text{weeks} / \text{minutes} = 10080$$ where the division of two time units results in a ratio in $\mathbb{R}_{\ge 0}$.

The ratio of the time unit `days` to the time unit `hours` is equal to the non-negative real number $24$.

The ratio of the time unit $\text{weeks}$ to the time unit $\text{hours}$ is equal to the non-negative real number $168$.