continuous

Mathlib.Topology.LocallyConstant.Basic

URI: https://scilib.ai/kg/mathlib#LocallyConstant.continuous

English

Every locally constant map f: X → Y is continuous.

Русский

Каждое локально константное отображение f: X → Y непрерывно.

LaTeX

$$$\\\\forall f:\\\\mathrm{LocallyConstant}(X,Y), \\\\mathrm{Continuous}(f)$$$

Lean4

protected theorem continuous : Continuous f :=
  f.isLocallyConstant.continuous

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

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

Разделы

Аффилиация

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