continuousOn

Mathlib.Topology.Covering

URI: https://scilib.ai/kg/mathlib#IsCoveringMapOn.continuousOn

English

A covering map restricted to preimage s is a continuous function on that set.

Русский

Покрывающее отображение, ограниченное до preimage s, непрерывно на этом множестве.

LaTeX

$$$\\text{ContinuousOn } f\\ (f^{-1}(s))$$$

Lean4

protected theorem continuousOn (hf : IsCoveringMapOn f s) : ContinuousOn f (f ⁻¹' s) :=
  continuousOn_of_forall_continuousAt fun _ ↦ hf.continuousAt

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

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

Разделы

Аффилиация

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