Physlib.Units.Examples

This definition represents a physical quantity of $400$ meters. It is constructed as a dimensionful value with the dimension of length $L_d$ and a numerical magnitude of $400$ within the International System of Units (SI).

Let $m$ be a physical quantity with the dimension of mass $M_{\text{d}}$, $E$ be a quantity with the dimension of energy $M_{\text{d}} L_{\text{d}}^2 T_{\text{d}}^{-2}$, and $c$ be a quantity with the dimension of velocity $L_{\text{d}} T_{\text{d}}^{-1}$. This definition represents the proposition that $E = m c^2$. Here, `WithDim D ℝ` denotes a real number associated with a specific physical dimension $D$.

The physical proposition $E = m c^2$ is dimensionally correct, where $m$ is a quantity with the dimension of mass $M_d$, $E$ is a quantity with the dimension of energy $M_d L_d^2 T_d^{-2}$, and $c$ is a quantity with the dimension of velocity $L_d T_d^{-1}$.

Let $M_d$, $L_d$, and $T_d$ represent the fundamental physical dimensions of mass, length, and time, respectively. This proposition defines the relationship between a mass $m$ with dimension $M_d$, a force $F$ with dimension $M_d L_d T_d^{-2}$, and an acceleration $a$ with dimension $L_d T_d^{-2}$ such that $F = m \cdot a$.

The proposition representing Newton's second law, $F = m \cdot a$, is dimensionally correct. Here, $m$ is a quantity with the dimension of mass $M_d$, $a$ is a quantity with the dimension of acceleration $L_d T_d^{-2}$, and $F$ is a quantity with the dimension of force $M_d L_d T_d^{-2}$, where $M_d$, $L_d$, and $T_d$ denote the fundamental dimensions of mass, length, and time, respectively.

Let $s$ be a real-valued quantity with dimensions of speed ($L \cdot T^{-1}$), $d$ be a quantity with dimensions of length ($L$), and $t$ be a quantity with dimensions of time ($T$). The proposition `SpeedEq` states that the speed $s$ is equal to the quotient of the distance $d$ and the time $t$, expressed as $s = d/t$.

The proposition $s = d/t$, where $s$ is a quantity with dimensions of speed ($L \cdot T^{-1}$), $d$ has dimensions of length ($L$), and $t$ has dimensions of time ($T$), is dimensionally correct.

Let $M_{\mathbf{d}}, L_{\mathbf{d}}, T_{\mathbf{d}}, \Theta_{\mathbf{d}}$, and $C_{\mathbf{d}}$ denote the dimensions of mass, length, time, temperature, and charge, respectively. Given the following quantities: - $m_1, m_2$ of dimension $M_{\mathbf{d}}$ - $\theta$ of dimension $\Theta_{\mathbf{d}}$ - $I_1, I_2$ of dimension $C_{\mathbf{d}} T_{\mathbf{d}}^{-1}$ - $d$ of dimension $L_{\mathbf{d}}$ - $t$ of dimension $T_{\mathbf{d}}$ - $X$ of dimension $L_{\mathbf{d}} T_{\mathbf{d}}^{-3} \Theta_{\mathbf{d}}^{-1} C_{\mathbf{d}}^2$ the proposition `OddDimensions` is defined by the equality: $$X = \frac{m_1 \cdot (d / t)}{m_2 \cdot \theta} \cdot I_2 \cdot I_1$$ This serves as an example of a dimensionally consistent relation involving complex combinations of physical dimensions.

The proposition `OddDimensions` is dimensionally correct. This proposition is defined for the following quantities: - $m_1, m_2$ with dimension of mass $M_{\mathbf{d}}$ - $\theta$ with dimension of temperature $\Theta_{\mathbf{d}}$ - $I_1, I_2$ with dimension of current (charge per time) $C_{\mathbf{d}} T_{\mathbf{d}}^{-1}$ - $d$ with dimension of length $L_{\mathbf{d}}$ - $t$ with dimension of time $T_{\mathbf{d}}$ - $X$ with dimension $L_{\mathbf{d}} T_{\mathbf{d}}^{-3} \Theta_{\mathbf{d}}^{-1} C_{\mathbf{d}}^2$ by the equality: $$X = \frac{m_1 \cdot (d / t)}{m_2 \cdot \theta} \cdot I_2 \cdot I_1$$ Dimensional correctness indicates that the physical dimensions of the expressions on both sides of the equality are identical.

Let $m$ be a real-valued quantity with mass dimension $M$, $E$ be a quantity with energy dimension $M L^2 T^{-2}$, and $c$ be a quantity with velocity dimension $L T^{-1}$. The proposition states that the underlying numerical value of $E$ is equal to the product of the numerical value of $m$ and the square of the numerical value of $c$, written as $E = mc^2$.

The proposition representing the relationship $E = mc^2$ is dimensionally correct, where $E$ is a physical quantity with energy dimensions $M L^2 T^{-2}$, $m$ is a quantity with mass dimension $M$, and $c$ is a quantity with velocity dimensions $L T^{-1}$.

This definition establishes a proposition for Newton's second law using physical quantities with associated dimensions. Given a mass $m$ with dimension $M$, a force $F$ with dimension $MLT^{-2}$, and an acceleration $a$ with dimension $LT^{-2}$ (where each is represented as a real-valued quantity using the `WithDim` structure), the proposition states that the underlying numerical value of the force is equal to the product of the underlying numerical values of the mass and the acceleration, i.e., $F = m \cdot a$.

The proposition representing Newton's second law, defined by the relation $F = m \cdot a$ for a force $F$ with dimensions $M L T^{-2}$, a mass $m$ with dimension $M$, and an acceleration $a$ with dimensions $L T^{-2}$, is dimensionally correct.

Given a mass $m$ with dimension $M$, an energy $E$ with dimension $M L^2 T^{-2}$, and a speed $c$ with dimension $L T^{-1}$, this proposition is defined by the equality of their underlying numerical values: $$E_{\text{val}} = m_{\text{val}} \cdot c_{\text{val}}$$ This represents a version of the energy-mass relation $E = mc$ that is dimensionally inconsistent, as the units of the left-hand side and right-hand side do not match.

The proposition $E = mc$, represented by the equality of numerical values $E_{\text{val}} = m_{\text{val}} \cdot c_{\text{val}}$, is not dimensionally correct, where $m$ is a mass with dimension $M$, $E$ is an energy with dimensions $M L^2 T^{-2}$, and $c$ is a speed with dimensions $L T^{-1}$.

Given a mass $m$ with dimension $M_d$, an energy $E$ with dimension $M_d L_d^2 T_d^{-2}$, and a system of unit choices $u$, this proposition asserts that the numerical value of $E$ is equal to the numerical value of $m$ multiplied by the square of the numerical value of the speed of light $c$ corresponding to the units $u$. In other words, it represents the equation $E = m c^2$.

Given a dimensionful mass $m$ (with dimension $M$) and a dimensionful energy $E$ (with dimension $M L^2 T^{-2}$), this proposition states that for a specific choice of units $u$, the numerical value of the energy $E$ in those units is equal to the product of the numerical value of the mass $m$ and the square of the numerical value of the speed of light $c$ in the same unit system $u$. Mathematically, this is expressed as $E(u) = m(u) \cdot c(u)^2$.

The proposition `EnergyMass`, which represents the mass-energy equivalence relation $E = mc^2$ involving a mass $m$ of dimension $M_d$, an energy $E$ of dimension $M_d L_d^2 T_d^{-2}$, and a choice of unit system $u$, is dimensionally correct.

In the International System of Units (SI), the mass-energy equivalence relation $E = mc^2$ holds for a mass $m$ with a numerical value of $2$ and an energy $E$ with a numerical value of $2 \times 299,792,458^2$.

For any system of unit choices $u$, the mass-energy equivalence relation $E = mc^2$ holds in system $u$ for a mass $m$ and an energy $E$ whose numerical values are obtained by scaling the SI values $m_{SI} = 2$ and $E_{SI} = 2 \times 299,792,458^2$ to the unit system $u$ using the `scaleUnit` function.

Given a value $t$ with the dimension of time $T$ and a value $\omega$ with the dimension of inverse time $T^{-1}$, this proposition asserts that the cosine of the product of their underlying numerical values is equal to a dimensionless real number $a$: $$\cos(\omega \cdot t) = a$$

The proposition defined by $\cos(\omega \cdot t) = a$ is dimensionally correct, where $t$ is a quantity with the dimension of time $T$, $\omega$ is a quantity with the dimension of inverse time $T^{-1}$, and $a$ is a dimensionless real number.