proj_isLocallyConstant

Mathlib.Topology.DiscreteQuotient

URI: https://scilib.ai/kg/mathlib#DiscreteQuotient.proj_isLocallyConstant

English

The projection π is locally constant.

Русский

Проекция π локально постоянна.

LaTeX

$$$ \\text{IsLocallyConstant}(\\pi)$$$

Lean4

theorem proj_isLocallyConstant : IsLocallyConstant S.proj :=
  (IsLocallyConstant.iff_continuous S.proj).2 S.proj_continuous

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

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

Разделы

Аффилиация

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