instSuccAddOrder

Mathlib.SetTheory.Ordinal.NaturalOps

URI: https://scilib.ai/kg/mathlib#NatOrdinal.instSuccAddOrder

English

NatOrdinal is endowed with a SuccAddOrder structure defined by x ↦ (nadd_one x)^{-1}.

Русский

NatOrdinal снабжается структурой SuccAddOrder, задаваемой отображением x ↦ (nadd_one x)^{-1}.

LaTeX

$$$\text{NatOrdinal}.\text{instSuccAddOrder} : \text{SuccAddOrder NatOrdinal} \;\text{defined by} \; x \mapsto (nadd\_one\ x)^{-1}$$$

Lean4

instance : SuccAddOrder NatOrdinal :=
  ⟨fun x => (nadd_one x).symm⟩

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

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

Разделы

Аффилиация

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