instFunLikeNat

Mathlib.Order.OmegaCompletePartialOrder

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

English

There is a canonical FunLike structure on Chain α with index set Nat.

Русский

Существует каноническая структура FunLike на Chain α индексированная NAT.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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