continuousAt

Mathlib.Topology.IsLocalHomeomorph

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

English

If f is a local homeomorph on s, then f is continuous at each x ∈ s.

Русский

Если f — локальный гомеоморфизм на s, то f непрерывна в каждой точке x∈s.

LaTeX

$$$IsLocalHomeomorphOn\\, f\\, s \\Rightarrow \\forall x\\in s, \\; ContinuousAt\\, f\\, x$$$

Lean4

protected theorem continuousAt (hf : IsLocalHomeomorphOn f s) {x : X} (hx : x ∈ s) : ContinuousAt f x :=
  (hf.map_nhds_eq hx).le

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

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

Разделы

Аффилиация

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