Shortcut instances for Lebesgue measure on real Euclidean spaces

The volume of EuclideanSpace ℝ (Fin n) is the measure of a finite-dimensional inner product space with its Borel structure, so each occurrence of volume re-derives the inner product, the finite dimension and the Borel structure. The shortcuts below record the measurable and measure space structures.

@[instance_reducible]

instance NavierStokesAndEuler.EuclideanSpaceShortcut.instMeasurableSpace {n : ℕ} : MeasurableSpace (EuclideanSpace ℝ (Fin n))

Shortcut for the Borel measurable structure of a real Euclidean space.

Equations

• NavierStokesAndEuler.EuclideanSpaceShortcut.instMeasurableSpace = inferInstance

instance NavierStokesAndEuler.EuclideanSpaceShortcut.instBorelSpace {n : ℕ} : BorelSpace (EuclideanSpace ℝ (Fin n))

Shortcut for the Borel property of a real Euclidean space.

@[instance_reducible]

noncomputable instance NavierStokesAndEuler.EuclideanSpaceShortcut.instMeasureSpace {n : ℕ} : MeasureTheory.MeasureSpace (EuclideanSpace ℝ (Fin n))

Shortcut for the Lebesgue measure space structure of a real Euclidean space.

Equations

• NavierStokesAndEuler.EuclideanSpaceShortcut.instMeasureSpace = inferInstance