diag — Mathlib

English

There is a diagonal embedding diag: α →o α × α given by diag(a) = (a,a). This is an order-homomorphism.

Русский

Существует диагональное вложение diag: α →o α × α, задающее diag(a) = (a,a). Это OrderHom.

LaTeX

$$$ diag = id \; \mathrm{.prod}\; id: \; \alpha \to^o \alpha \times \alpha. $$$

Lean4

/-- Diagonal embedding of `α` into `α × α` as an `OrderHom`. -/
@[simps!]
def diag : α →o α × α :=
  id.prod id

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