Intervals avoiding a finite family of real points

A finite family of real points is bounded above, so an open interval beyond it contains a point.

theorem TauCeti.exists_Ioo_disjoint_range_of_finite {ι : Type u_1} [Finite ι] (a : ι → ℝ) : ∃ (p : ℝ) (q : ℝ) (x : ℝ), (∀ (i : ι), a i ∉ Set.Ioo p q) ∧ x ∈ Set.Ioo p q

There is a nonempty open real interval avoiding a finite family of real points.