isCoveringMap_iff_isCoveringMapOn_univ

English

A map is a covering map if and only if it is a covering map on the entire space.

Русский

Отображение является покрывающим тогда и только тогда, когда оно покрывает всю пространство.

LaTeX

$$$IsCoveringMap f \\Leftrightarrow IsCoveringMapOn f Set.univ$$$

Lean4

theorem isCoveringMap_iff_isCoveringMapOn_univ : IsCoveringMap f ↔ IsCoveringMapOn f Set.univ := by
  simp only [IsCoveringMap, IsCoveringMapOn, Set.mem_univ, forall_true_left]

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