cons' — Mathlib

English

This defines an operation cons' on Sym' by mapping each class of a vector to the class of the vector with a prepended element a.

Русский

Определяется операция cons' на Sym': отображение каждого класса вектора в класс вектора с добавлением элемента a в начало.

LaTeX

$$$ \mathrm{cons'}(a, [v]) = [\mathrm{Vector.cons}(a, v)]. $$$

Lean4

/-- This is `cons` but for the alternative `Sym'` definition.
-/
def cons' {α : Type*} {n : ℕ} : α → Sym' α n → Sym' α (Nat.succ n) := fun a =>
  Quotient.map (Vector.cons a) fun ⟨_, _⟩ ⟨_, _⟩ h => List.Perm.cons _ h

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