E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ {x | EMetric.infEdist x s < ENNReal.ofReal δ}⁻¹ = {x | EMetric.infEdist x⁻¹ s < ENNReal.ofReal δ}
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ (thickening δ s)⁻¹ = thickening δ s⁻¹
simp_rw [thickening, ← infEdist_inv]
no goals
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ {x | EMetric.infEdist x s < ENNReal.ofReal δ}⁻¹ = {x | EMetric.infEdist x⁻¹ s < ENNReal.ofReal δ}
rfl