nth_injective

Mathlib.Data.Nat.Nth

URI: https://scilib.ai/kg/mathlib#Nat.nth_injective

English

If hf is infinite, then nth p is an injective function.

Русский

Если hf бесконечно, то nth p — инъективная функция.

LaTeX

$$Injective (Nat.nth p)$$

Lean4

theorem nth_injective (hf : (setOf p).Infinite) : Function.Injective (nth p) :=
  (nth_strictMono hf).injective

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

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

Разделы

Аффилиация

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