id — Mathlib · SciLib

English

The identity map on α extends to a bounded-order homomorphism α → α.

Русский

Идентичное отображение на множестве α является гомоморфизмом ограниченного порядка от α к α.

LaTeX

$$$\mathrm{BoundedOrderHom}.id(\alpha) : \mathrm{BoundedOrderHom}(\alpha,\alpha)$$$

Lean4

/-- `id` as a `BoundedOrderHom`. -/
protected def id : BoundedOrderHom α α :=
  { OrderHom.id, TopHom.id α, BotHom.id α with }

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