map_pred

Mathlib.Order.SuccPred.InitialSeg

URI: https://scilib.ai/kg/mathlib#PrincipalSeg.map_pred

English

Analogously, f(pred a) = pred (f a).

Русский

Аналогично, f(pred a) = pred(f a).

LaTeX

$$$f(\operatorname{pred}a) = \operatorname{pred}(f(a))$$$

Lean4

theorem map_pred [PredOrder α] [NoMinOrder α] [PredOrder β] (f : α ≤i β) (a : α) : f (pred a) = pred (f a) :=
  (f : α ≤i β).map_pred a

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

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

Разделы

Аффилиация

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