dist on `real`

Stream: Is there code for X?

[Scott Morrison]

Do we have

lemma foo (a b ε : ℝ) : dist a b < ε ↔ a < b + ε ∧ b - ε < a :=

or some close variation? (e.g. I don't mind if the RHS is a < b + ε ∧ b < a + ε or similar)

[Shing Tak Lam]

lemma foo (a b ε : ℝ) : dist a b < ε ↔ a - b < ε ∧ b - a < ε := abs_sub_lt_iff

[Patrick Massot]

import topology.instances.real

lemma foo (a b ε : ℝ) : dist a b < ε ↔ b - ε < a ∧ a < b + ε :=
by simp [← metric.mem_ball, real.ball_eq_Ioo]