Theorems · Theorem · measure theory
AntilipschitzWith.le_dimH_image
∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] {K : NNReal} {f : X → Y},
AntilipschitzWith K f → ∀ (s : Set X), dimH s ≤ dimH (f '' s)- Cited by
- 1 results in Mathlib
- Foundations
- Depth 207 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- EMetricSpaceEMetricSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- ENNRealstatement · cited by 9,879
- Set.imagestatement and proof · cited by 5,609
- NNRealstatement and proof · cited by 4,310
- EMetricSpacestatement and proof · cited by 242
- AntilipschitzWithstatement and proof · cited by 132
- dimHstatement · cited by 65
- Set.subset_preimage_imageproof · cited by 44
- dimH_monoproof · cited by 8
- AntilipschitzWith.dimH_preimage_leproof · cited by 1
Cited by1
Results whose statement or proof uses this declaration.
- Isometry.dimH_imageproof · cited by 2