Theorems · Inductive type · general topology
Metric.Snowflaking
Type u_1 → (α : ℝ) → 0 < α → α ≤ 1 → Type u_1
A copy of a type with metric given by dist x y = (dist x.val y.val) ^ α.
This is defined as a one-field structure.
- Defined in
- Mathlib.Topology.MetricSpace.Snowflaking
- Cited by
- 65 results in Mathlib
- Foundations
- Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
Cited by77
Results whose statement or proof uses this declaration.
- Metric.Snowflaking.toSnowflakingstatement · cited by 41
- Metric.Snowflaking.ofSnowflakingstatement · cited by 41
- Metric.Snowflaking.image_ofSnowflaking_eq_preimagestatement and proof · cited by 6
- Metric.Snowflaking.image_toSnowflaking_eq_preimagestatement · cited by 6
- Metric.Snowflaking.toSnowflaking_ofSnowflakingstatement and proof · cited by 4
- Metric.Snowflaking.valstatement and proof · cited by 4
- Metric.Snowflaking.casesOnstatement and proof · cited by 4
- Metric.Snowflaking.uniformEquivstatement and proof · cited by 3
- Metric.Snowflaking.homeomorphstatement and proof · cited by 3
- Metric.Snowflaking.preimage_toSnowflaking_closedEBallstatement and proof · cited by 2
- Metric.Snowflaking.preimage_toSnowflaking_eballstatement and proof · cited by 2
- Metric.Snowflaking.image_toSnowflaking_closedEBallstatement and proof · cited by 2