When dealing with proofs, I have the following conceptual problem.
Imagine that, in proving a certain statement, we assume the continuity of a certain function $f: X \to Y$ at point $x_0$. This means that we are assuming that $$\forall \varepsilon > 0 \ \exists \delta > 0: \forall y \in X \ \big( \ |x_0 - y| < \delta \implies |f(x_0)- f(y)| < \varepsilon \ \big).$$
Considering this is something we are assuming, we can proceed with universal instantiation about $\varepsilon$, and we can pick whatever $\varepsilon > 0$ we want.
Question:
Can we proceed with a form of (sort of) reverse engineering, and pick a specific $\varepsilon > 0$ that gives rise to a $\bar{\delta}$ that makes a fortiori $d(x_0, y^*) < \delta$ true for a specific $y^*$ we care about, without actually describing it explicitly?
[In a proof this should read as "Take a $\varepsilon > 0$, such that there is a $\bar{\delta}>0$, such that $d(x_0, y^*) < \bar{\delta}$".]
I am not completely sure, because the order in which quantifiers are dealed in this way looks a bit peculiar to me.
I am looking forward to any feedback.
Thank you for your time.