pred_ne_pred_iff

Mathlib.Order.SuccPred.Basic

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

English

For all a,b, pred a ≠ pred b iff a ≠ b.

Русский

Для любых a,b предшественник a не равен предшественнику b тогда и только тогда, когда a не равен b.

LaTeX

$$$ pred\\ a \\neq pred\\ b \\iff a \\neq b $$$

Lean4

theorem pred_ne_pred_iff : pred a ≠ pred b ↔ a ≠ b :=
  pred_injective.ne_iff

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

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

Разделы

Аффилиация

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