PhyslibSearch

Physlib.Electromagnetism.Dynamics.Basic

8 declarations

theorem

0≤ϵ00 \le \epsilon_0

#ε₀_nonneg

For any free space F\mathcal{F} with electric permittivity ϵ0\epsilon_0, it holds that 0≤ϵ00 \le \epsilon_0.

theorem

0≤μ00 \le \mu_0

#μ₀_nonneg

For any free space F\mathcal{F} with magnetic permeability μ0\mu_0, it holds that 0≤μ00 \le \mu_0.

theorem

ϵ0≠0\epsilon_0 \neq 0

#ε₀_ne_zero

For any free space F\mathcal{F} with electric permittivity ϵ0\epsilon_0, it holds that ϵ0≠0\epsilon_0 \neq 0.

theorem

μ0≠0\mu_0 \neq 0

#μ₀_ne_zero

For any free space F\mathcal{F} with magnetic permeability μ0\mu_0, it holds that μ0≠0\mu_0 \neq 0.

definition

Speed of light c=1/ϵ0μ0c = 1/\sqrt{\epsilon_0 \mu_0} in free space

#c

Given a free space F\mathcal{F} with electric permittivity ϵ0\epsilon_0 and magnetic permeability μ0\mu_0, the speed of light cc is defined by the relation c=1ϵ0μ0c = \frac{1}{\sqrt{\epsilon_0 \mu_0}} This definition includes a proof that cc is a positive value, as required by the `SpeedOfLight` type.

theorem

c=1/ϵ0μ0c = 1/\sqrt{\epsilon_0 \mu_0}

#c_val

For any free space F\mathcal{F} with electric permittivity ϵ0\epsilon_0 and magnetic permeability μ0\mu_0, the speed of light cc is given by the relation c=1ϵ0μ0c = \frac{1}{\sqrt{\epsilon_0 \mu_0}}

theorem

c2=1ϵ0μ0c^2 = \frac{1}{\epsilon_0 \mu_0}

#c_sq

For any free space F\mathcal{F} with electric permittivity ϵ0\epsilon_0 and magnetic permeability μ0\mu_0, the square of the speed of light cc is given by the relation c2=1ϵ0μ0c^2 = \frac{1}{\epsilon_0 \mu_0}

theorem

∣c∣=c|c| = c for the speed of light in free space

#c_abs

For any free space F\mathcal{F}, the speed of light cc in that space satisfies the property that its absolute value is equal to itself, i.e., ∣c∣=c|c| = c.