no goals
α : Type u_1
β : Type ?u.65221
inst✝ : PseudoMetricSpace α
x y z : α
s t : Set α
hs : Set.Nontrivial s
⊢ infsep s = ⨅ (d : ↑(offDiag s)), uncurry dist ↑d
classical rw [Set.infsep_eq_iInf, if_pos hs]
no goals
α : Type u_1
β : Type ?u.65221
inst✝ : PseudoMetricSpace α
x y z : α
s t : Set α
hs : Set.Nontrivial s
⊢ infsep s = ⨅ (d : ↑(offDiag s)), uncurry dist ↑d
rw [Set.infsep_eq_iInf, if_pos hs]