instPredSubOrder

Mathlib.Data.Nat.SuccPred

URI: https://scilib.ai/kg/mathlib#Nat.instPredSubOrder

English

ℕ carries a PredSubOrder structure with the standard predecessor operation.

Русский

ℕ имеет структуру PredSubOrder, в которой предшественник — обычная операция.

LaTeX

$$$\\\\text{PredSubOrder}(\\\\mathbb N) \\\\text{ with } \\\\operatorname{pred} = \\operatorname{pred}_{\\\\mathbb N}.$$$

Lean4

instance instPredSubOrder : PredSubOrder ℕ :=
  ⟨fun _ => rfl⟩

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

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

Разделы

Аффилиация

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