α : Type u_1
β : Type ?u.59186
inst✝ : PseudoMetricSpace α
x y z : α
s t : Set α
d : ℝ
hs : Set.Nontrivial s
⊢ ¬infsep s < d ↔ ¬∃ x x_1 y x_2 _hxy, dist x y < d
α : Type u_1
β : Type ?u.59186
inst✝ : PseudoMetricSpace α
x y z : α
s t : Set α
d : ℝ
hs : Set.Nontrivial s
⊢ infsep s < d ↔ ∃ x x_1 y x_2 _hxy, dist x y < d
rw [← not_iff_not]
α : Type u_1
β : Type ?u.59186
inst✝ : PseudoMetricSpace α
x y z : α
s t : Set α
d : ℝ
hs : Set.Nontrivial s
⊢ d ≤ infsep s ↔ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → d ≤ dist x y
α : Type u_1
β : Type ?u.59186
inst✝ : PseudoMetricSpace α
x y z : α
s t : Set α
d : ℝ
hs : Set.Nontrivial s
⊢ ¬infsep s < d ↔ ¬∃ x x_1 y x_2 _hxy, dist x y < d
push_neg
no goals
α : Type u_1
β : Type ?u.59186
inst✝ : PseudoMetricSpace α
x y z : α
s t : Set α
d : ℝ
hs : Set.Nontrivial s
⊢ d ≤ infsep s ↔ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → d ≤ dist x y
exact hs.le_infsep_iff