Theorems · Theorem · measure theory

AlternatingMap.measure_parallelepiped

∀ {G : Type u_3} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] [inst_2 : MeasurableSpace G]
  [inst_3 : BorelSpace G] [inst_4 : FiniteDimensional ℝ G] {n : ℕ} [_i : Fact (Module.finrank ℝ G = n)]
  (ω : G [⋀^Fin n]→ₗ[ℝ] ℝ) (v : Fin n → G), ω.measure (parallelepiped v) = ENNReal.ofReal |ω v|

Defined in

Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Cited by

1 results in Mathlib

Foundations

Depth 260 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceMeasurableSpaceBorelSpaceFiniteDimensionalFact