cons_injective_of_injective — Mathlib

English

If x0 is not in the range of x and x is injective, then the function cons x0 x is injective.

Русский

Если x0 не принадлежит образу x и x инъективна, то функция cons x0 x инъективна.

LaTeX

$$$\\text{cons\_injective\_of\_injective}\\;\\{\\alpha\\} (x_0) (x : Fin n \\to \\alpha) (hx_0 : x_0 \\notin \\mathrm{range}(x)) (hx : \\mathrm{Injective}(x)) : \\mathrm{Injective}(\\\\mathrm{cons}(x_0,x))$$$

Lean4

theorem cons_injective_of_injective {α} {x₀ : α} {x : Fin n → α} (hx₀ : x₀ ∉ Set.range x) (hx : Function.Injective x) :
    Function.Injective (cons x₀ x : Fin n.succ → α) := by
  intro i j
  cases i using Fin.cases <;> cases j using Fin.cases <;> aesop (add simp [hx.eq_iff])

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