Theory HOL-Analysis.Cartesian_Space
section "Linear Algebra on Finite Cartesian Products"
theory Cartesian_Space
imports
"HOL-Combinatorics.Transposition"
Finite_Cartesian_Product
Linear_Algebra
begin
subsection ‹Type @{typ ‹'a ^ 'n›} and fields as vector spaces›
definition "cart_basis = {axis i 1 | i. i∈UNIV}"
lemma finite_cart_basis: "finite (cart_basis)" unfolding cart_basis_def
using finite_Atleast_Atmost_nat by fastforce
lemma card_cart_basis: "card (cart_basis::('a::zero_neq_one^'i) set) = CARD('i)"
unfolding cart_basis_def Setcompr_eq_image
by (rule card_image) (auto simp: inj_on_def axis_eq_axis)