cons_right_injective — Mathlib

English

Let M be a type with a zero, and y ∈ M. The map cons_y: (Fin n →₀ M) → Fin (n+1) →₀ M, which appends the coordinate n with value y, is injective: if cons_y(t) = cons_y(t′) then t = t′.

Русский

Пусть M — множество с нулём, и y ∈ M. Отображение cons_y: (Fin n →₀ M) → Fin (n+1) →₀ M, добавляющее координату n со значением y, инъективно: если cons_y(t) = cons_y(t′), то t = t′.

LaTeX

$$$\\forall t,t'.\\; cons_y(t) = cons_y(t') \\Rightarrow t = t'$,$$

Lean4

theorem cons_right_injective {n : ℕ} {M : Type*} [Zero M] (y : M) :
    Injective (Finsupp.cons y : (Fin n →₀ M) → Fin (n + 1) →₀ M) :=
  (equivFunOnFinite.symm.injective.comp ((Fin.cons_right_injective _).comp DFunLike.coe_injective))

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