Theorems · Theorem · measure theory
Real.dimH_univ_pi_fin
∀ (n : ℕ), dimH Set.univ = ↑n
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 252 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- ENNRealstatement and proof · cited by 9,879
- Set.univstatement · cited by 3,945
- Fintype.card_finproof · cited by 270
- dimHstatement · cited by 65
- Real.dimH_univ_piproof · cited by 1
Cited by1
Results whose statement or proof uses this declaration.
- Real.dimH_of_mem_nhdsproof · cited by 3