Finsupp.cons, Finsupp.snoc and their lexicographic comparison

Finsupp.cons x s : Fin (n + 1) →₀ M puts x in front of s. Adding two of them adds heads and tails separately. The lexicographic order compares the entries at 0 first, so two of them are compared by their heads, and then by their tails.

Dually, Finsupp.snoc s x : Fin (n + 1) →₀ M appends x after s, and Finsupp.init t forgets the last entry of t; these are the Finsupp versions of Fin.snoc and Fin.init. Adding two such vectors adds initial parts and last entries separately. Two such vectors are compared lexicographically by their initial parts first, and then by their last entries.

theorem Finsupp.cons_add_cons {n : ℕ} {M : Type u_1} [AddZeroClass M] (x y : M) (s t : Fin n →₀ M) : cons x s + cons y t = cons (x + y) (s + t)

theorem Finsupp.toLex_cons_lt_toLex_cons_iff {n : ℕ} {M : Type u_1} [Zero M] [LT M] {x y : M} {s t : Fin n →₀ M} : toLex (cons x s) < toLex (cons y t) ↔ x < y ∨ x = y ∧ toLex s < toLex t

Strict lexicographic comparison of Finsupp.cons compares the heads first and compares the tails when the heads are equal.

noncomputable def Finsupp.snoc {n : ℕ} {M : Type u_1} [Zero M] (s : Fin n →₀ M) (y : M) : Fin (n + 1) →₀ M

Finsupp.snoc s y : Fin (n + 1) →₀ M appends y after s. See Fin.snoc.

Equations

• s.snoc y = Finsupp.equivFunOnFinite.symm (Fin.snoc (⇑s) y)

noncomputable def Finsupp.init {n : ℕ} {M : Type u_1} [Zero M] (t : Fin (n + 1) →₀ M) : Fin n →₀ M

Finsupp.init t : Fin n →₀ M forgets the last entry of t. See Fin.init.

Equations

• t.init = Finsupp.equivFunOnFinite.symm (Fin.init ⇑t)

@[simp]

theorem Finsupp.coe_snoc {n : ℕ} {M : Type u_1} [Zero M] (s : Fin n →₀ M) (y : M) : ⇑(s.snoc y) = Fin.snoc (⇑s) y

@[simp]

theorem Finsupp.coe_init {n : ℕ} {M : Type u_1} [Zero M] (t : Fin (n + 1) →₀ M) : ⇑t.init = Fin.init ⇑t

theorem Finsupp.snoc_castSucc {n : ℕ} {M : Type u_1} [Zero M] (s : Fin n →₀ M) (y : M) (i : Fin n) : (s.snoc y) i.castSucc = s i

theorem Finsupp.snoc_last {n : ℕ} {M : Type u_1} [Zero M] (s : Fin n →₀ M) (y : M) : (s.snoc y) (Fin.last n) = y

theorem Finsupp.init_apply {n : ℕ} {M : Type u_1} [Zero M] (t : Fin (n + 1) →₀ M) (i : Fin n) : t.init i = t i.castSucc

@[simp]

theorem Finsupp.init_snoc {n : ℕ} {M : Type u_1} [Zero M] (s : Fin n →₀ M) (y : M) : (s.snoc y).init = s

@[simp]

theorem Finsupp.snoc_init_self {n : ℕ} {M : Type u_1} [Zero M] (t : Fin (n + 1) →₀ M) : t.init.snoc (t (Fin.last n)) = t

@[simp]

theorem Finsupp.snoc_zero_zero {n : ℕ} {M : Type u_1} [Zero M] : snoc 0 0 = 0

theorem Finsupp.snoc_injective2 {n : ℕ} {M : Type u_1} [Zero M] : Function.Injective2 snoc

@[simp]

theorem Finsupp.snoc_inj {n : ℕ} {M : Type u_1} [Zero M] {s s' : Fin n →₀ M} {y y' : M} : s.snoc y = s'.snoc y' ↔ s = s' ∧ y = y'

theorem Finsupp.eq_snoc_iff {n : ℕ} {M : Type u_1} [Zero M] {t : Fin (n + 1) →₀ M} {s : Fin n →₀ M} {y : M} : t = s.snoc y ↔ t.init = s ∧ t (Fin.last n) = y

theorem Finsupp.toLex_snoc_lt_toLex_snoc_iff {n : ℕ} {M : Type u_1} [Zero M] [LT M] {x y : M} {s t : Fin n →₀ M} : toLex (s.snoc x) < toLex (t.snoc y) ↔ toLex s < toLex t ∨ s = t ∧ x < y

Strict lexicographic comparison of Finsupp.snoc compares the initial parts first and compares the last entries when the initial parts are equal.

theorem Finsupp.snoc_add_snoc {n : ℕ} {M : Type u_1} [AddZeroClass M] (s t : Fin n →₀ M) (x y : M) : s.snoc x + t.snoc y = (s + t).snoc (x + y)