Theorems · Definition · measure theory

Module.Basis.parallelepiped

{ι : Type u_1} →
  {E : Type u_3} →
    [Fintype ι] →
      [inst : NormedAddCommGroup E] →
        [inst_1 : NormedSpace ℝ E] → Module.Basis ι ℝ E → TopologicalSpace.PositiveCompacts E

The parallelepiped spanned by a basis, as a compact set with nonempty interior.

Defined in: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Cited by: 12 results in Mathlib
Foundations: Depth 171 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Fintype NormedAddCommGroup NormedSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coeproof · cited by 62,936
Realstatement and proof · cited by 25,697
NormedAddCommGroupstatement and proof · cited by 15,752
NormedSpacestatement and proof · cited by 12,499
Fintypestatement and proof · cited by 7,736
Module.Basisstatement and proof · cited by 1,477
TopologicalSpace.PositiveCompactsstatement · cited by 112
parallelepipedproof · cited by 25

Cited by12

Results whose statement or proof uses this declaration.

Module.Basis.addHaar_defstatement and proof · cited by 7
Module.Basis.map_addHaarproof · cited by 5
Module.Basis.addHaar_eq_iffstatement and proof · cited by 5
Module.Basis.parallelepiped_basisFunstatement and proof · cited by 3
Module.Basis.coe_parallelepipedstatement · cited by 2
Module.Basis.parallelepiped_mapstatement · cited by 1
Module.Basis.parallelepiped_reindexstatement · cited by 1
Module.Basis.prod_parallelepipedstatement · cited by 1
Orientation.measure_eq_volumeproof · cited by 1
Real.volume_eq_stieltjes_idproof · cited by 1
Module.Basis.parallelepiped_eq_mapstatement and proof · cited by 0
IsZLattice.isCompact_range_of_periodicproof · cited by 0