id — Mathlib · SciLib

English

The identity map on α, viewed as a ContinuousOrderHom, is the identity transformation.

Русский

Идентичное отображение на α, рассмотренное как ContinuousOrderHom, совпадает с тождественным преобразованием.

LaTeX

$$$\text{ContinuousOrderHom.id }\alpha : \alpha \toCo \alpha$ is the identity map.$$

Lean4

/-- `id` as a `ContinuousOrderHom`. -/
protected def id : α →Co α :=
  ⟨OrderHom.id, continuous_id⟩

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