id

Mathlib.Order.OmegaCompletePartialOrder

URI: https://scilib.ai/kg/mathlib#OmegaCompletePartialOrder.ωScottContinuous.id

English

The identity map on any type is ωScott-continuous.

Русский

Идентичное отображение на любом множестве является ωScott-непрерывным.

LaTeX

$$$$ \omegaScottContinuous(\text{id} : \alpha \to \alpha). $$$$

Lean4

theorem id : ωScottContinuous (id : α → α) :=
  ScottContinuousOn.id

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

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

Разделы

Аффилиация

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