# Proof that the inverse image of a single element is a discrete space

Let $$f: X \rightarrow Y$$ be a local homeomorphism. I want to prove that, for each $$y \in Y$$, the fiber $$f^{-1}(y)$$ is a discrete set, or discrete space (Is there any difference between these two last terms?).
These are the posts I have read so far:

Local homeomorphism and inverse image

When is a local homeomorphism a covering map?

Showing the fibre over a point in a covering map is a discrete space.

How do I show that a topological space is discrete if all its subsets are closed?

Show that in a discrete metric space, every subset is both open and closed.

However, I have not been able to fully understand the proof. Some of the posts start the proof by mentioning that the fact that $$f$$ is a local homeomorphism implies that the fiber is finite; but I do not understand where does that come from, even after browsing MathSE and Wikipedia.
Other posts try instead to prove that the fiber is finite, and they do so by first stating that the fiber is a discrete space. All of this make it look like circular reasoning, which does not make sense to me.
If there is a concept I do not know, I am willing to visit places like Wikipedia or Subwiki.org ; however this time I have not been able to understand the proof even after reading many articles.

So, how can I prove this?

Fix $$y\in Y$$ and $$x\in f^{-1}(y)$$. Since $$f$$ is a local homeomorphism, there is a neighborhood $$U$$ of $$x$$ such that $$f|U : U\to f(U)$$ is a homeomorphism. If $$z\in U\cap f^{-1}(y)$$, then $$f(z) = y = f(x)$$; since both $$z, x\in U$$, injectivity of $$f|U$$ implies $$z = x$$. Therefore $$U\cap f^{-1}(y) = \{x\}$$. As $$x$$ was arbitrary, $$f^{-1}(y)$$ is discrete.
Let $$f:X \to Y$$ be a local homeomorphism.
Suppose $$y \in Y$$ and let $$x \in F_y:=f^{-1}[\{y\}]$$, the fibre of $$y$$.
Then $$x$$ has an open neighbourhood $$U_x$$ such that $$f|_{U_x}: U_x \to f[U_x]$$ is a homeomorphism (by the definition of being a local homeomorphism).
In particular, $$U_x \cap F_y = \{x\}$$ or else we have some $$x' \in U_x \cap F_y$$ which means $$f(x')=f(x)=y$$ while $$x,x' \in U_x$$ contradicting the fact that $$f|_{U_x}$$ is injective (being a homeomorphism). So $$U_x$$ witnesses that $$x$$ is an isolated point of $$F_y$$, showing that $$F_y$$ is indeed discrete in the subspace topology.