case h
ι : Type ?u.61211
α : Type u
β : Type v
γ : Type w
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
hf : Isometry f
x : α
p : ℝ → Prop
y : α
⊢ y ∈ f ⁻¹' {y | p (dist y (f x))} ↔ y ∈ {y | p (dist y x)}
ι : Type ?u.61211
α : Type u
β : Type v
γ : Type w
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
hf : Isometry f
x : α
p : ℝ → Prop
⊢ f ⁻¹' {y | p (dist y (f x))} = {y | p (dist y x)}
ext y
no goals
case h
ι : Type ?u.61211
α : Type u
β : Type v
γ : Type w
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
hf : Isometry f
x : α
p : ℝ → Prop
y : α
⊢ y ∈ f ⁻¹' {y | p (dist y (f x))} ↔ y ∈ {y | p (dist y x)}
simp [hf.dist_eq]