instOrderHomClassNat

Mathlib.Order.OmegaCompletePartialOrder

URI: https://scilib.ai/kg/mathlib#OmegaCompletePartialOrder.Chain.instOrderHomClassNat

English

There is a canonical OrderHomClass instance for Chain α from Nat to α.

Русский

Существует канонический экземпляр OrderHomClass для Chain α от Nat к α.

LaTeX

$$$\\text{OrderHomClass}(\\text{Chain}(\\alpha), \\mathbb{N}, \\alpha)$$$

Lean4

instance : OrderHomClass (Chain α) ℕ α :=
  inferInstanceAs <| OrderHomClass (ℕ →o α) ℕ α

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru