Theorems · Theorem · general topology

Metric.Snowflaking.image_toSnowflaking_closedEBall

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

Defined in

Mathlib.Topology.MetricSpace.Snowflaking

Cited by

2 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpace