empty_val' — Mathlib

English

For any α and any n', and any j, the i-th slice of the empty array equals the empty array.

Русский

Для любых α и n' и любого j, i-й разрез пустого массива равен пустому массиву.

LaTeX

$$$\forall {\alpha} {n' : Type} (j : n'), \ (\text{fun } i \Rightarrow (![] : \mathrm{Fin} 0 \to n' \to \alpha)\, i\, j) = ![]$$$

Lean4

theorem empty_val' {n' : Type*} (j : n') : (fun i => (![] : Fin 0 → n' → α) i j) = ![] :=
  empty_eq _

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