isCoveringMapOn

Mathlib.Topology.Covering

URI: https://scilib.ai/kg/mathlib#IsCoveringMap.isCoveringMapOn

English

A covering map is continuous on the preimage of its codomain.

Русский

Покрывающее отображение непрерывно на подмножество предобраза кодом.

LaTeX

$$$IsCoveringMapOn f Set.univ\\Rightarrow\\text{ContinuousOn } f (f^{-1}(Set.univ))$$$

Lean4

protected theorem isCoveringMapOn (hf : IsCoveringMap f) : IsCoveringMapOn f Set.univ :=
  isCoveringMap_iff_isCoveringMapOn_univ.mp hf

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru