id

Mathlib.Order.OrdContinuous

URI: https://scilib.ai/kg/mathlib#RightOrdContinuous.id

English

The identity map id: α → α is RightOrdContinuous for any preorder α.

Русский

Идентичная функция id: α → α является правой непрерывной на любом предпорядке α.

LaTeX

$$$ \\mathrm{RightOrdContinuous}(\\mathrm{id}_{\\alpha}) $$$

Lean4

protected theorem id : RightOrdContinuous (id : α → α) := fun s x h => by simpa only [image_id] using h

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

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

Разделы

Аффилиация

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