hasForgetToFinPartOrd — Mathlib

English

There is a forgetful functor from NonemptyFinLinOrd to FinPartOrd, forgetting the lattice-linear order structure and producing a finite-partial-order.

Русский

Существует функтор забывания из NonemptyFinLinOrd в FinPartOrd, забывающий линейно-упорядоченную структуру и переходящий к конечному частично упорядоченному множеству.

LaTeX

$$$ \text{HasForget}_{\text{NonemptyFinLinOrd}, \text{FinPartOrd}}. $$$

Lean4

instance hasForgetToFinPartOrd : HasForget₂ NonemptyFinLinOrd FinPartOrd
    where
  forget₂.obj X := .of X
  forget₂.map f := FinPartOrd.ofHom f.hom

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