English
Let f:E → X be as above. Suppose there exists, for every x ∈ X, a trivialization e_x of the family F x such that x ∈ baseSet(e_x). Then f is a covering map.
Русский
Пусть f:E → X, и для каждого x ∈ X существует тривиализация e_x семейства F x над f, удовлетворяющая x ∈ baseSet(e_x). Тогда f является покровным отображением.
LaTeX
$$$\text{Let } f:E\to X.\ \text{If } \forall x\in X,\ \exists e_x:\, \text{Trivialization}(F_x)\ f, \ x\in (e_x).\text{baseSet}, \text{ then } f\text{ is a covering map.}$$$
Lean4
theorem mk (F : X → Type*) [∀ x, TopologicalSpace (F x)] [∀ x, DiscreteTopology (F x)] (e : ∀ x, Trivialization (F x) f)
(h : ∀ x, x ∈ (e x).baseSet) : IsCoveringMap f :=
isCoveringMap_iff_isCoveringMapOn_univ.mpr <| .mk _ _ _ _ fun x ↦ h x
