rcons_injective — Mathlib

English

For a fixed i, the map rcons(i,·) from Pair d i to NormalWord d is injective.

Русский

Для фиксированного i отображение rcons(i,·) из пары d i в NormalWord d инъективно.

LaTeX

$$$$\\forall i,\\; \\mathrm{Function.Injective} (rcons(i) : \\mathrm{Pair}\\, d\, i \\to \\mathrm{NormalWord}\, d).$$$$

Lean4

theorem rcons_injective {i : ι} : Function.Injective (rcons (d := d) i) :=
  by
  rintro ⟨⟨head₁, tail₁⟩, _⟩ ⟨⟨head₂, tail₂⟩, _⟩
  simp only [rcons, NormalWord.mk.injEq, EmbeddingLike.apply_eq_iff_eq, Word.Pair.mk.injEq, Pair.mk.injEq, and_imp]
  intro h₁ h₂ h₃
  subst h₂
  rw [← equiv_fst_mul_equiv_snd (d.compl i) head₁, ← equiv_fst_mul_equiv_snd (d.compl i) head₂, h₁, h₃]
  simp

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