Speed

In this module we define the dimensionful type corresponding to an speed. We define specific insances of speed, such as miles per hour, kilometers per hour, etc.

@[reducible, inline]

abbrev DimSpeed : Type

The type of speeds in the absence of a choice of unit.

Equations

• DimSpeed = Dimensionful (Dimension.L𝓭 * Dimension.T𝓭⁻¹) NNReal

Basic speeds

noncomputable def DimSpeed.oneMeterPerSecond : DimSpeed

The dimensional speed corresponding to 1 meter per second.

Equations

• DimSpeed.oneMeterPerSecond = Dimensionful.ofUnit (Dimension.L𝓭 * Dimension.T𝓭⁻¹) 1 UnitChoices.SI

noncomputable def DimSpeed.oneMilePerHour : DimSpeed

The dimensional speed corresponding to 1 mile per hour.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DimSpeed.oneKilometerPerHour : DimSpeed

The dimensional speed corresponding to 1 kilometer per hour.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DimSpeed.oneKnot : DimSpeed

The dimensional speed corresponding to 1 knot, aka, one nautical mile per hour.

Equations

• One or more equations did not get rendered due to their size.

Speed in SI units

@[simp]

theorem DimSpeed.oneMeterPerSecond_in_SI : ↑oneMeterPerSecond UnitChoices.SI = 1

@[simp]

theorem DimSpeed.oneMilePerHour_in_SI : ↑oneMilePerHour UnitChoices.SI = 0.44704

@[simp]

theorem DimSpeed.oneKilometerPerHour_in_SI : ↑oneKilometerPerHour UnitChoices.SI = 5 / 18

@[simp]

theorem DimSpeed.oneKnot_in_SI : ↑oneKnot UnitChoices.SI = 463 / 900

Relations between speeds

theorem DimSpeed.oneKnot_eq_mul_oneKilometerPerHour : oneKnot = 1.852 • oneKilometerPerHour

theorem DimSpeed.oneKilometerPerHour_eq_mul_oneKnot : oneKilometerPerHour = (250 / 463) • oneKnot

theorem DimSpeed.oneMeterPerSecond_eq_mul_oneMilePerHour : oneMeterPerSecond = (3125 / 1397) • oneMilePerHour

Comparisons between speeds

theorem DimSpeed.oneKilometerPerHour_le_oneKnot : oneKilometerPerHour ≤ oneKnot

One kilometer per hour is slower then one knot.

theorem DimSpeed.oneKilometerPerHour_le_oneMilPerHour : oneKilometerPerHour ≤ oneMilePerHour

theorem DimSpeed.oneMilePerHour_le_oneKnot : oneMilePerHour ≤ oneKnot

theorem DimSpeed.oneMilePerHour_le_oneMeterPerSecond : oneMilePerHour ≤ oneMeterPerSecond

theorem DimSpeed.oneMeterPerSecond_le_oneKnot : oneKnot ≤ oneMeterPerSecond