Every fibre of a local injection is discrete

Let $𝑓 : 𝑋 \to 𝑌$ be a local injection. Then $𝑓 - 1 {𝑦}$ is a discrete subspace of $𝑋$ for every $𝑦 \in 𝑌$ . #m/thm/topology

Proof

Let $𝑦 \in 𝑌$ and $𝑥 1, 𝑥 2 \in 𝑓 - 1 {𝑦}$ , so that $𝑓 (𝑥 1) = 𝑓 (𝑥 2) = 𝑦$ $𝑥 1$ and $𝑥 2$ have open neighbourhoods $𝑈$ and $𝑉$ respectively such that $𝑓 ↾ 𝑈$ and $𝑓 ↾ 𝑉$ are injections: Thus $𝑈 \cap 𝑓 - 1 {𝑦} = {𝑥 1}$ and $𝑉 \cap 𝑓 - 1 {𝑦} = {𝑥 2}$ . Since $𝑈$ and $𝑉$ are open in $𝑋$ , the singletons ${𝑥 1}$ and ${𝑥 2}$ are open in the subspace topology of the fibre $𝑓 - 1 {𝑦}$ . The selection of $𝑥 1, 𝑥 2 \in 𝑓 - 1 {𝑦}$ was arbitrary, therefore $𝑓 - 1 {𝑦}$ carries a discrete topology for any $𝑦 \in 𝑌$ .

#state/tidy | #lang/en | #SemBr