case inl
ι : Sort ?u.66671
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
t u : Set α
x y : α
Φ : α → β
h : ¬x ∈ closure ∅
⊢ ContinuousAt (fun x => (infDist x ∅)⁻¹) x

case inr
ι : Sort ?u.66671
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
h : ¬x ∈ closure s
hs : Set.Nonempty s
⊢ ContinuousAt (fun x => (infDist x s)⁻¹) x
ι : Sort ?u.66671
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
h : ¬x ∈ closure s
⊢ ContinuousAt (fun x => (infDist x s)⁻¹) x
rcases s.eq_empty_or_nonempty with (rfl | hs)
no goals
case inl
ι : Sort ?u.66671
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
t u : Set α
x y : α
Φ : α → β
h : ¬x ∈ closure ∅
⊢ ContinuousAt (fun x => (infDist x ∅)⁻¹) x
simp only [infDist_empty, continuousAt_const]
case inr
ι : Sort ?u.66671
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
h : ¬x ∈ closure s
hs : Set.Nonempty s
⊢ infDist x s ≠ 0
case inr
ι : Sort ?u.66671
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
h : ¬x ∈ closure s
hs : Set.Nonempty s
⊢ ContinuousAt (fun x => (infDist x s)⁻¹) x
refine (continuous_infDist_pt s).continuousAt.inv₀ ?_
no goals
case inr
ι : Sort ?u.66671
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
h : ¬x ∈ closure s
hs : Set.Nonempty s
⊢ infDist x s ≠ 0
rwa [Ne.def, ← mem_closure_iff_infDist_zero hs]