Theorems · Definition · general topology
Metric.Snowflaking.toSnowflaking
{X : Type u_1} → {α : ℝ} → {hα₀ : 0 < α} → {hα₁ : α ≤ 1} → X ≃ Metric.Snowflaking X α hα₀ hα₁The natural equivalence between X and Snowflaking X α hr₀ hr₁.
- Defined in
- Mathlib.Topology.MetricSpace.Snowflaking
- Cited by
- 41 results in Mathlib
- Foundations
- Depth 99 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- Equivstatement · cited by 8,337
- Equiv.symmproof · cited by 3,681
- Metric.Snowflakingstatement · cited by 65
- Metric.Snowflaking.ofSnowflakingproof · cited by 41
Cited by42
Results whose statement or proof uses this declaration.
- Metric.Snowflaking.image_ofSnowflaking_eq_preimagestatement · cited by 6
- Metric.Snowflaking.image_toSnowflaking_eq_preimagestatement and proof · cited by 6
- Metric.Snowflaking.toSnowflaking_ofSnowflakingstatement · cited by 4
- 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
- Metric.Snowflaking.image_toSnowflaking_eballstatement and proof · cited by 2
- Metric.Snowflaking.preimage_ofSnowflaking_closedEBallstatement · cited by 2
- Metric.Snowflaking.preimage_ofSnowflaking_eballstatement · cited by 2
- Metric.Snowflaking.preimage_toSnowflaking_ballstatement and proof · cited by 1
- Metric.Snowflaking.preimage_toSnowflaking_closedBallstatement and proof · cited by 1
- Metric.Snowflaking.casesOn_toSnowflakingstatement and proof · cited by 1