PhyslibSearch

Physlib.Relativity.SpeedOfLight

6 declarations

instance

Coercion from `SpeedOfLight` to R\mathbb{R}

#instCoeReal

This definition provides a coercion from the `SpeedOfLight` type to the real numbers R\mathbb{R}. It allows a value representing the speed of light to be automatically treated as its underlying numerical value in R\mathbb{R}.

instance

Speed of light c=1c = 1

#instOne

This definition provides an instance of the speed of light with a numerical value of 11. It represents the unit speed of light in a system of units (such as natural units) where the speed of light in vacuum is normalized to c=1c = 1.

theorem

The numerical value of the unit speed of light is 11

#val_one

The numerical value of the unit speed of light constant 11 in the `SpeedOfLight` type is equal to 11.

theorem

The speed of light is strictly positive (c>0c > 0)

#val_pos

Let cc be a speed of light in vacuum. Its representation as a real number is strictly positive, i.e., c>0c > 0.

theorem

The speed of light is non-negative (c≥0c \ge 0)

#val_nonneg

Let cc be a speed of light in a vacuum. Its representation as a real number is non-negative, i.e., c≥0c \ge 0.

theorem

The speed of light is non-zero (c≠0c \neq 0)

#val_ne_zero

Let cc be a speed of light in a vacuum. Then, its representation as a real number is non-zero, i.e., c≠0c \neq 0.