IsCoveringMap — Mathlib

English

A covering map is a function that is continuous with discrete fibers and every point has an evenly covered neighborhood.

Русский

Покрывающее отображение — непрерывное отображение с дискретными волокнами и у каждого x есть равномерно покрытое окрестность.

LaTeX

$$$IsCoveringMap\\ f := (\\forall x, IsEvenlyCovered f x (f^{-1}\\{x\\}))$$$

Lean4

/-- A covering map is a continuous function `f : E → X` with discrete fibers such that each point
  of `X` has an evenly covered neighborhood. -/
def IsCoveringMap :=
  ∀ x, IsEvenlyCovered f x (f ⁻¹' { x })

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