ext — Mathlib

English

There is a canonical bijection between functions f: m → n → α and matrices Matrix m n α; this is realized by translating f into a matrix of its values.

Русский

Существует каноническая биекция между функциями f: m → n → α и матрицами Matrix m n α; она реализуется преобразованием f в матрицу значений f.

LaTeX

$$$(m \\to n \\to α) \\cong Matrix m n α$$

Lean4

@[ext]
theorem ext : (∀ i j, M i j = N i j) → M = N :=
  ext_iff.mp

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