pred_ofMul

Mathlib.Algebra.Order.SuccPred.TypeTags

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

English

For any X with a preorder and PredOrder, pred toMul x equals (pred x) toMul.

Русский

Для любого X с предпорядком и PredOrder pred к виду toMul x равен toMul от pred x.

LaTeX

$$$$\operatorname{pred}(x^{\text{toMul}}) = (\operatorname{pred} x)^{\text{toMul}}$$$$

Lean4

@[simp]
theorem pred_ofMul [Preorder X] [PredOrder X] (x : X) : pred (ofMul x) = ofMul (pred x) :=
  rfl

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

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

Разделы

Аффилиация

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