uniqueFromBot — Mathlib

English

In any preorder with a bottom element, there is a unique morphism from the bottom element to every x in the set; i.e., the hom-set from ⊥ to x is a singleton.

Русский

В частично упорядоченном множестве с наименьшим элементом существует единственный морфизм из нижнего элемента в произвольный x; то есть множество стрел ⊥ → x содержит ровно один элемент.

LaTeX

$$$\forall x:\,X\;\#\mathrm{Hom}(\perp, x) = 1$$$

Lean4

instance uniqueFromBot [OrderBot X] {x : X} : Unique (⊥ ⟶ x)
    where
  default := homOfLE bot_le
  uniq := fun a => by rfl

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