Units on Temperature #
A unit of temperature corresponds to a choice of translationally-invariant
metric on the temperature manifold (to be defined diffeomorphic to ℝ≥0
).
Such a choice is (non-canonically) equivalent to a
choice of positive real number. We define the type TemperatureUnit
to be equivalent to the
positive reals.
On TemperatureUnit
there is an instance of division giving a real number, corresponding to the
ratio of the two scales of temperature unit.
To define specific temperature units, we first axiomise the existence of a a given temperature unit, and then construct all other temperature units from it. We choose to axiomise the existence of the temperature unit of kelvin, and construct all other temperature units from that.
Equations
- TemperatureUnit.instInhabited = { default := { val := 1, property := TemperatureUnit.instInhabited._proof_1 } }
Division of TemperatureUnit #
Equations
- TemperatureUnit.instHDivNNReal = { hDiv := fun (x t : TemperatureUnit) => ⟨x.val / t.val, ⋯⟩ }
The scaling of a temperature unit #
The scaling of a temperature unit by a positive real.
Instances For
Specific choices of temperature units #
To define a specific temperature units, we must first axiomise the existence of a a given temperature unit, and then construct all other temperature units from it. We choose to axiomise the existence of the temperature unit of kelvin.
We need an axiom since this relates something to something in the physical world.
The axiom corresponding to the definition of a temperature unit of kelvin.
The temperature unit of degrees nanokelvin (10^(-9) kelvin).
Equations
Instances For
The temperature unit of degrees microkelvin (10^(-6) kelvin).
Equations
Instances For
The temperature unit of degrees millikelvin (10^(-3) kelvin).
Equations
Instances For
The temperature unit of degrees fahrenheit ((5/9) of a kelvin).
Note, this is fahrenheit starting at 0
absolute temperature.