IsCoveringMap.isSeparatedMap
theorem IsCoveringMap.isSeparatedMap :
∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X},
IsCoveringMap f → IsSeparatedMap f
The theorem states that for any two types `E` and `X`, both equipped with topological spaces, if a function `f` from `E` to `X` is a covering map, then it is also a separated map. In other words, in a covering map, any two distinct points in `E` with the same image in `X` can be separated by open neighborhoods. This quantifies over all possible mappings and topological spaces for the types `E` and `X`.
More concisely: Given types `E` and `X` with topological spaces, if `f` is a covering map from `E` to `X`, then for any distinct points `x, y` in `E` with `f(x) = f(y)`, there exist open neighborhoods `U` of `x` and `V` of `y` such that `U ∩ V = ∅`.
|
IsCoveringMap.isLocalHomeomorph
theorem IsCoveringMap.isLocalHomeomorph :
∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X},
IsCoveringMap f → IsLocalHomeomorph f
This theorem states that for any types `E` and `X` equipped with topological space structures and for any function `f` from `E` to `X`, if `f` is a covering map (i.e., it is continuous, its fibers are discrete, and each point in `X` has an evenly covered neighborhood), then `f` is also a local homeomorphism. In other words, each point in `E` is contained in the source of some partial homeomorphism from `E` to `X` that coincides with `f`.
More concisely: If `f` : `E` → `X` is a continuous function between topological spaces `E` and `X` such that `f` is a covering map (i.e., its fibers are discrete and each point in `X` has an evenly covered neighborhood), then `f` is a local homeomorphism.
|