Theorems · Theorem · general topology

Metric.Snowflaking.image_toSnowflaking_closedBall

∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : PseudoMetricSpace X] (x : X) {r : ℝ},
  0 ≤ r →
    ⇑Metric.Snowflaking.toSnowflaking '' Metric.closedBall x r =
      Metric.closedBall (Metric.Snowflaking.toSnowflaking x) (r ^ α)

Defined in

Mathlib.Topology.MetricSpace.Snowflaking

Cited by

1 results in Mathlib

Foundations

Depth 218 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PseudoMetricSpace