isInitialBot — Mathlib

English

In a preordered type, the bottom element is initial in the associated category.

Русский

В предопорядоченном типе нижний элемент является начальнoм в соответствующей категории.

LaTeX

$$$ \\text{isInitial}(\\perp) \\text{ in the category associated to the preorder}. $$$

Lean4

/-- The least element in a preordered type is initial in the category
associated to this preorder. -/
def isInitialBot : IsInitial (⊥ : C) :=
  IsInitial.ofUnique _

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