map_pred

Mathlib.Order.SuccPred.Basic

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

English

If f is an order isomorphism, it commutes with pred: f(pred a) = pred(f a).

Русский

Если f — упорядоченная биекции, сохраняющая порядок, то f(pred a) = pred(f a).

LaTeX

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

Lean4

theorem _root_.OrderIso.map_pred {β : Type*} [PartialOrder β] [PredOrder β] (f : α ≃o β) (a : α) :
    f (pred a) = pred (f a) :=
  f.dual.map_succ a

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

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

Разделы

Аффилиация

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