injective_permutations'Aux — Mathlib

English

For every x, the function permutations'Aux x is injective: if permutations'Aux x s = permutations'Aux x t, then s = t.

Русский

Для каждого x функция permutations'Aux x инъективна: если permutations'Aux x s = permutations'Aux x t, то s = t.

LaTeX

$$$\forall x,\, \operatorname{Function.Injective}(\operatorname{permutations'Aux} x)$$$

Lean4

theorem injective_permutations'Aux (x : α) : Function.Injective (permutations'Aux x) :=
  by
  intro s t h
  apply insertIdx_injective s.length x
  dsimp
  have hl : s.length = t.length := by simpa using congr_arg length h
  rw [← get_permutations'Aux s x s.length (by simp), ← get_permutations'Aux t x s.length (by simp [hl])]
  simp only [get_eq_getElem, h, hl]

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