Separated and locally injective maps

A continuous separated map f : X → Y separates the points of each fibre by disjoint open sets, and continuity pulls back the separation of points with distinct images when Y is Hausdorff. So the source of a continuous separated map to a Hausdorff space is Hausdorff. Covering maps are separated (IsCoveringMap.isSeparatedMap), so the total space of a covering of a Hausdorff space is Hausdorff.

The fibers of a locally injective map are discrete (IsLocallyInjective.isDiscrete_preimage_singleton), so a compact subset of one fiber is finite (IsLocallyInjective.finite_preimage_singleton_inter); this needs no topology on the codomain. For a separated, locally injective map, such as a covering map or any locally injective map with Hausdorff total space, two sections over a preconnected set that are continuous on that set and agree at one of its points agree on all of it (IsSeparatedMap.eqOn_of_leftInvOn).

theorem IsSeparatedMap.t2Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : X → Y} (sep : IsSeparatedMap f) (hf : Continuous f) : T2Space X

The source of a continuous separated map to a Hausdorff space is Hausdorff.

theorem IsCoveringMap.t2Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : X → Y} (hf : IsCoveringMap f) : T2Space X

The total space of a covering of a Hausdorff space is Hausdorff.

theorem IsLocallyInjective.isDiscrete_preimage_singleton {E : Type u_3} {B : Type u_4} [TopologicalSpace E] {p : E → B} (hp : IsLocallyInjective p) (b : B) : IsDiscrete (p ⁻¹' {b})

The fibers of a locally injective map, such as a local homeomorphism, are discrete.

theorem IsLocallyInjective.finite_preimage_singleton_inter {E : Type u_3} {B : Type u_4} [TopologicalSpace E] {p : E → B} (hp : IsLocallyInjective p) {s : Set E} {b : B} (hs : IsCompact (p ⁻¹' {b} ∩ s)) : (p ⁻¹' {b} ∩ s).Finite

A compact set of points in one fiber of a locally injective map, such as a local homeomorphism, is finite.

theorem IsSeparatedMap.eqOn_of_leftInvOn {E : Type u_3} {B : Type u_4} [TopologicalSpace E] {p : E → B} [TopologicalSpace B] (sep : IsSeparatedMap p) (hinj : IsLocallyInjective p) {S : Set B} {s s' : B → E} (hS : IsPreconnected S) (hs : ContinuousOn s S) (hs' : ContinuousOn s' S) (hl : Set.LeftInvOn p s S) (hl' : Set.LeftInvOn p s' S) {y : B} (hy : y ∈ S) (hee' : s y = s' y) : Set.EqOn s s' S

Two sections of p over a preconnected set S that are continuous on S and agree at one point of S agree on S, when p is separated and locally injective. Every map with Hausdorff total space is separated (T2Space.isSeparatedMap), and so is every covering map (IsCoveringMap.isSeparatedMap).