snoc_left_injective — Mathlib

English

For fixed p, the right argument of snoc is injective; i.e., the map i ↦ (snoc p i) is injective.

Русский

Для фиксированного p правая часть snoc инъективна; отображение i ↦ snoc p i инъективно.

LaTeX

$$$\\mathrm{snoc\\_right\\_injective} : \\forall p, \\mathrm{Function.Injective}(\\mathrm{snoc}\\ p)$$$

Lean4

theorem snoc_left_injective (xₙ : α (last n)) : Function.Injective (snoc · xₙ) :=
  snoc_injective2.left _

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