succ_ofMul

Mathlib.Algebra.Order.SuccPred.TypeTags

URI: https://scilib.ai/kg/mathlib#Order.succ_ofMul

English

For all X with Preorder and SuccOrder, and all x in X, succ(ofMul x) = ofMul (succ x).

Русский

Для любого X с предордером и порядком следования, и любого x в X, succ(ofMul x) = ofMul (succ x).

LaTeX

$$succ (ofMul x) = ofMul (succ x)$$

Lean4

@[simp]
theorem succ_ofMul [Preorder X] [SuccOrder X] (x : X) : succ (ofMul x) = ofMul (succ x) :=
  rfl

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

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

Разделы

Аффилиация

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