hasForgetToLinOrd — Mathlib

English

There is a forgetful functor from NonemptyFinLinOrd to LinOrd, forgetting the lattice structure and retaining the underlying order.

Русский

Существует функтор забывания из NonemptyFinLinOrd в LinOrd, забывающий решеточную структуру и сохраняя исходный порядок.

LaTeX

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

Lean4

instance hasForgetToLinOrd : HasForget₂ NonemptyFinLinOrd LinOrd :=
  InducedCategory.hasForget₂ _

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