insertNth_injective2 — Mathlib

English

For fixed p, the binary function insertNth p is injective in its two arguments: if p.insertNth x_p x = p.insertNth y_p y, then x_p = y_p and x = y.

Русский

Для фиксированного p операция p.insertNth является инъективной по обеим аргументам: если p.insertNth x_p x = p.insertNth y_p y, то x_p = y_p и x = y.

LaTeX

$$∀ {x_p y_p x y}, \ p.insertNth x_p x = p.insertNth y_p y \Rightarrow x_p = y_p ∧ x = y$$

Lean4

/-- As a binary function, `Fin.insertNth` is injective. -/
theorem insertNth_injective2 {p : Fin (n + 1)} : Function.Injective2 (@insertNth n α p) := fun xₚ yₚ x y h ↦
  ⟨by simpa using congr_fun h p, funext fun i ↦ by simpa using congr_fun h (succAbove p i)⟩

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