English
If a fiber bundle F over E with a family of trivializations exists for every x ∈ X such that x ∈ baseSet of the trivialization at x, then the projection πF E is a covering map.
Русский
Пусть F над E образует семейство тривиализаций для каждого x ∈ X, причём x принадлежит базовому множеству соответствующей тривиализации. Тогда проецирующее отображение πF E является покровным отображением.
LaTeX
$$$\forall x:\, X,\ \exists e:\ Trivialization(F,f),\ x\in e.baseSet\Rightarrow IsCoveringMap(\pi F E)$$$
Lean4
protected theorem isCoveringMap {F : Type*} [TopologicalSpace F] [DiscreteTopology F]
(hf : ∀ x : X, ∃ e : Trivialization F f, x ∈ e.baseSet) : IsCoveringMap f :=
IsCoveringMap.mk f (fun _ => F) (fun x => Classical.choose (hf x)) fun x => Classical.choose_spec (hf x)
