equal
deleted
inserted
replaced
8 imports |
8 imports |
9 Euclidean_Space |
9 Euclidean_Space |
10 L2_Norm |
10 L2_Norm |
11 "HOL-Library.Numeral_Type" |
11 "HOL-Library.Numeral_Type" |
12 "HOL-Library.Countable_Set" |
12 "HOL-Library.Countable_Set" |
|
13 "HOL-Library.FuncSet" |
13 begin |
14 begin |
14 |
15 |
15 subsection \<open>Finite Cartesian products, with indexing and lambdas\<close> |
16 subsection \<open>Finite Cartesian products, with indexing and lambdas\<close> |
16 |
17 |
17 typedef ('a, 'b) vec = "UNIV :: ('b::finite \<Rightarrow> 'a) set" |
18 typedef ('a, 'b) vec = "UNIV :: ('b::finite \<Rightarrow> 'a) set" |