cons_left_injective

Mathlib.Data.Seq.Defs

URI: https://scilib.ai/kg/mathlib#Stream'.Seq.cons_left_injective

English

For fixed s, the map x ↦ cons x s is injective.

Русский

При фиксированном s отображение x ↦ cons x s инъективно.

LaTeX

$$$\\forall s:\\mathrm{Seq}\\alpha,\\; \\mathrm{Function.Injective}(\\lambda x, \\mathrm{cons}\\ x\\ s).$$$

Lean4

theorem cons_left_injective (s : Seq α) : Function.Injective fun x => cons x s :=
  cons_injective2.left _

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

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

Разделы

Аффилиация

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