Theorems · Theorem · general topology

Isometry.preimage_setOfPred_dist

∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β},
  Isometry f → ∀ (x : α) (p : ℝ → Prop), f ⁻¹' {y | p (dist y (f x))} = {y | p (dist y x)}

Defined in

Mathlib.Topology.MetricSpace.Isometry

Cited by

4 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpacePseudoMetricSpace