ofIsEmpty — Mathlib

English

There exists a trivial embedding from an empty order to any preorder β.

Русский

Существуют тривиальные вложения из пустого множества в любую предпорядок.

LaTeX

$$$\exists e:\alpha \hookrightarrow_o \beta$ (при условии IsEmpty α)$$

Lean4

/-- The trivial embedding from an empty preorder to another preorder -/
@[simps]
def ofIsEmpty [IsEmpty α] : α ↪o β where
  toFun := isEmptyElim
  inj' := isEmptyElim
  map_rel_iff' {a} := isEmptyElim a

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