Theorems · Theorem · measure theory
Module.Basis.parallelepiped_basisFun
∀ (ι : Type u_1) [inst : Fintype ι], (Pi.basisFun ℝ ι).parallelepiped = TopologicalSpace.PositiveCompacts.piIcc01 ι
The parallelepiped formed from the standard basis for ι → ℝ is [0,1]^ι
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 172 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Fintype
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites17
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setproof · cited by 53,352
- Realstatement and proof · cited by 25,697
- SetLike.coeproof · cited by 8,199
- Fintypestatement and proof · cited by 7,736
- Latticeproof · cited by 916
- Pi.singleproof · cited by 518
- Set.uIccproof · cited by 393
- SetLike.coe_injectiveproof · cited by 374
- zero_le_oneproof · cited by 316
- TopologicalSpace.PositiveCompactsstatement · cited by 112
- Pi.basisFunstatement and proof · cited by 78
- Set.uIcc_of_leproof · cited by 54
Cited by3
Results whose statement or proof uses this declaration.
- EuclideanSpace.volume_preserving_symm_measurableEquiv_toLpproof · cited by 4
- Complex.volume_preserving_equiv_piproof · cited by 2
- Module.Basis.parallelepiped_eq_mapproof · cited by 0