α : Type u_1
β : Type ?u.24010
inst✝ : EDist α
x y : α
s t : Set α
⊢ ∀ (i : α), i ∈ s → x ≠ i → einfsep (insert x s) ≤ edist x i
α : Type u_1
β : Type ?u.24010
inst✝ : EDist α
x y : α
s t : Set α
⊢ einfsep (insert x s) ≤ ⨅ (y : α) (_ : y ∈ s) (_ : x ≠ y), edist x y
simp_rw [le_iInf_iff]
no goals
α : Type u_1
β : Type ?u.24010
inst✝ : EDist α
x y : α
s t : Set α
⊢ ∀ (i : α), i ∈ s → x ≠ i → einfsep (insert x s) ≤ edist x i
refine' fun _ hy hxy => einfsep_le_edist_of_mem (mem_insert _ _) (mem_insert_of_mem _ hy) hxy