snoc_right_injective — Mathlib

English

For any fixed last component, the function snoc · x_n is injective.

Русский

Для фиксированной последней компоненты функция snoc · x_n инъективна по первому аргументу.

LaTeX

$$$\\mathrm{snoc\\_left\\_injective} : \\forall x_n, \\mathrm{Function.Injective}(\\mathrm{snoc}\\;\\cdot\\; x_n)$$$

Lean4

theorem snoc_right_injective (x : ∀ i : Fin n, α i.castSucc) : Function.Injective (snoc x) :=
  snoc_injective2.right _

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