cons_injective2 — Mathlib

English

The constructor cons is injective in both arguments: if cons x s = cons y t, then x=y and s=t.

Русский

Конструктор cons инъективен по обеим переменным: если cons x s = cons y t, тогда x=y и s=t.

LaTeX

$$$\\forall {\\alpha} \\forall {\\beta} \\; \\text{Function.Injective2}(\\mathrm{cons} : \\alpha \\to \\mathrm{Seq}\\ \\alpha \\to \\mathrm{Seq}\\ \\alpha).$$$

Lean4

theorem cons_injective2 : Function.Injective2 (cons : α → Seq α → Seq α) := fun x y s t h =>
  ⟨by rw [← Option.some_inj, ← get?_cons_zero, h, get?_cons_zero],
    Seq.ext fun n => by simp_rw [← get?_cons_succ x s n, h, get?_cons_succ]⟩

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