nth_injOn

Mathlib.Data.Nat.Nth

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

English

If hf is finite, then the function nth p is injective on the interval {x : x < #hf.toFinset.card}.

Русский

Если hf конечное, то nth p инъективна на множестве {x : x < |hf.toFinset|}.

LaTeX

$$(Set.Iio #hf.toFinset).InjOn (nth p)$$

Lean4

theorem nth_injOn (hf : (setOf p).Finite) : (Set.Iio #hf.toFinset).InjOn (nth p) :=
  (nth_strictMonoOn hf).injOn

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

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

Разделы

Аффилиация

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