id

Mathlib.Topology.Order.Hom.Esakia

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

English

Identity morphism acts as identity with respect to Esakia morphisms.

Русский

Единичный морфизм действует как тождественный для всех морфизмов Эзякия.

LaTeX

$$$\\text{EsakiaHom}.id(\\alpha)$ acts as identity: f \\circ \\text{id} = f$$$

Lean4

/-- `id` as an `EsakiaHom`. -/
protected def id : EsakiaHom α α :=
  ⟨ContinuousOrderHom.id α, fun _ b h => ⟨b, h, rfl⟩⟩

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

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

Разделы

Аффилиация

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