English
Let f: E → X be a map between topological spaces. Suppose there exists a family of local trivializations t_x (one for each x in range(f)) with base sets containing x, together with a family F x of discrete-topology fibers, and suppose range(f) is closed in X. Then f is a covering map.
Русский
Пусть f: E → X — отображение между топологическими пространствами. Предположим существование семейства локальных тривиализаций t_x (для каждого x ∈ range(f)) с базовыми областями, содержащими x, совместно с семейством фибр F x, где для всех x задана топология F x как дискретная. Если образ range(f) замкнут в X, тогда f является покровным отображением.
LaTeX
$$$\text{Let } f:E\to X.\ \text{Assume there exists a family }(t_x)_{x\in\operatorname{range}(f)} \text{ with } t_x\text{ a trivialization and } x\in t_x\text{ baseSet, and }\operatorname{range}(f)\text{ is closed in }X. \text{Then } f\ \text{is a covering map.}$$$
Lean4
/-- A constructor for `IsCoveringMap` when there are both empty and nonempty fibers. -/
theorem mk' (F : X → Type*) [∀ x, TopologicalSpace (F x)] [∀ x, DiscreteTopology (F x)]
(t : ∀ x, x ∈ Set.range f → { t : Trivialization (F x) f // x ∈ t.baseSet }) (h : IsClosed (Set.range f)) :
IsCoveringMap f :=
isCoveringMap_iff_isCoveringMapOn_univ.mpr <|
.mk' f _ _ (fun x h ↦ t x h) fun _x hx ↦
⟨_, h.isOpen_compl.mem_nhds hx, Set.eq_empty_of_forall_notMem fun x h ↦ h ⟨x, rfl⟩⟩
