α : Type u_1
β : Type ?u.56359
inst✝ : EDist α
x y : α
s : Set α
hxy : x ≠ y
⊢ ENNReal.toReal (edist x y ⊓ edist y x) ≤ ENNReal.toReal (edist x y ⊓ edist y x)
α : Type u_1
β : Type ?u.56359
inst✝ : EDist α
x y : α
s : Set α
hxy : x ≠ y
⊢ infsep {x, y} ≤ ENNReal.toReal (edist x y ⊓ edist y x)
simp_rw [infsep, einfsep_pair_eq_inf hxy]
no goals
α : Type u_1
β : Type ?u.56359
inst✝ : EDist α
x y : α
s : Set α
hxy : x ≠ y
⊢ ENNReal.toReal (edist x y ⊓ edist y x) ≤ ENNReal.toReal (edist x y ⊓ edist y x)
simp