Documentation

Complexity.Foundations.Data.Fin.Tuple

Appending constant tuples #

The addition of Christian Reitwiessner's branch crei/tidy-universal (and of cslib PR #1112) to Cslib.Foundations.Data.Fin.Tuple: appending constant tuples gives a constant tuple.

theorem Fin.append_const {α : Sort u_1} {m n : ℕ} (x : α) :
(append (fun (x_1 : Fin m) => x) fun (x_1 : Fin n) => x) = fun (x_1 : Fin (m + n)) => x

Appending two constant tuples gives a constant tuple.