isCoveringMap — Mathlib

English

For a fiber bundle with total space being the product of a base and fiber, the projection map is a covering map.

Русский

Для фибробандла сумма пространства является произведением базового пространства и фибры; проекция является покровным отображением.

LaTeX

$$$\text{IsCoveringMap}(\pi F E)$$$

Lean4

protected theorem isCoveringMap {F : Type*} {E : X → Type*} [TopologicalSpace F] [DiscreteTopology F]
    [TopologicalSpace (Bundle.TotalSpace F E)] [∀ x, TopologicalSpace (E x)] [FiberBundle F E] :
    IsCoveringMap (π F E) :=
  IsFiberBundle.isCoveringMap fun x => ⟨trivializationAt F E x, mem_baseSet_trivializationAt F E x⟩

Похожие утверждения