succ_injective

Mathlib.Order.SuccPred.Basic

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

English

The successor map is injective on a linear order with no maximal elements.

Русский

Отображение следующего элемента инъективно на линейном упорядочении без максимума.

LaTeX

$$$\text{Injective}(\operatorname{succ} : \alpha \to \alpha)$$$

Lean4

theorem succ_injective : Injective (succ : α → α) := fun _ _ => succ_eq_succ_iff.1

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

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

Разделы

Аффилиация

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