enumOrd_injective

Mathlib.SetTheory.Ordinal.Enum

URI: https://scilib.ai/kg/mathlib#Ordinal.enumOrd_injective

English

If s is not bounded above, then enumOrd s is injective.

Русский

Если s не ограничено сверху, то enumOrd s инъективен.

LaTeX

$$$\forall s,\ \neg BddAbove\, s \Rightarrow \text{Injective}(\operatorname{enumOrd} s)$$$

Lean4

theorem enumOrd_injective (hs : ¬BddAbove s) : Function.Injective (enumOrd s) :=
  (enumOrd_strictMono hs).injective

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

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

Разделы

Аффилиация

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