Imports
/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module
public import Mathlib.Data.Real.BasicThe Speed of Light
i. Overview
In this module we define a type for the speed of light in a vacuum, along with some basic properties. An element of this type is a positive real number, and should be thought of as the speed of light in some chosen but arbitrary system of units.
ii. Key results
SpeedOfLight : The type of speeds of light in a vacuum.
iii. Table of contents
A. The Speed of Light type
B. Instances on the type
C. The instance of one
D. Positivity properties
iv. References
@[expose] public sectionA. The Speed of Light type
The speed of light in a vacuum. An element of this type should be thought of as the speed of light in some chosen but arbitrary system of units.
The underlying value of the speed of light.
structure SpeedOfLight where val : ℝ
pos : 0 < valB. Instances on the type
instance : Coe SpeedOfLight ℝ := ⟨SpeedOfLight.val⟩C. The instance of one
We define the instance of one for SpeedOfLight to be the speed of light equal to 1.
This is useful when we are working in units where the speed of light is equal to one.
instance : One SpeedOfLight := ⟨1, ⊢ 0 < 1 All goals completed! 🐙⟩@[simp]
lemma val_one : (1 : SpeedOfLight).val = 1 := rflD. Positivity properties
@[simp]
lemma val_pos (c : SpeedOfLight) : 0 < (c : ℝ) := c.pos@[simp]
lemma val_nonneg (c : SpeedOfLight) : 0 ≤ (c : ℝ) := le_of_lt c.pos@[simp]
lemma val_ne_zero (c : SpeedOfLight) : (c : ℝ) ≠ 0 := ne_of_gt c.pos