English
The set of matrices with entries in S can be viewed as the preimage, under the natural isomorphism between matrices and functions, of the product of copies of S indexed by rows and columns.
Русский
Множество матриц с элементами из S можно рассматривать как прообраз под естественным изоморфизмом между матрицами и функциями от индексов до S, то есть как произведение копий S по индексам строк и столбцов.
LaTeX
$$$S.matrix = \\mathrm{of.symm}^{-1}'\\mathrm Set.univ.pi (\\lambda (\\_,) : m \\mapsto Set.univ.pi (\\lambda (\\_,) \\mapsto S))$$$
Lean4
theorem matrix_eq_pi {S : Set α} : S.matrix = of.symm ⁻¹' Set.univ.pi fun (_ : m) ↦ Set.univ.pi fun (_ : n) ↦ S :=
by
ext
simp [Set.mem_matrix]
