continuousOn

Mathlib.Topology.IsLocalHomeomorph

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

English

From local homeomorph on s, we obtain a continuous function on s as a whole.

Русский

Из локального гомеоморфизма на s следует непрерывность на всём s.

LaTeX

$$$IsLocalHomeomorphOn\\, f\\, s \\Rightarrow ContinuousOn\\, f\\, s$$$

Lean4

protected theorem continuousOn (hf : IsLocalHomeomorphOn f s) : ContinuousOn f s :=
  continuousOn_of_forall_continuousAt fun _x ↦ hf.continuousAt

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

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

Разделы

Аффилиация

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