cons_right_injective

Mathlib.Data.Seq.Defs

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

English

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

Русский

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

LaTeX

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

Lean4

theorem cons_right_injective (x : α) : Function.Injective (cons x) :=
  cons_injective2.right _

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

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

Разделы

Аффилиация

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