| changeset 66453 | cc19f7ca2ed6 |
| parent 63910 | e4fdf9580372 |
| 66452:450cefec7c11 | 66453:cc19f7ca2ed6 |
|---|---|
3 *) |
3 *) |
4 |
4 |
5 section \<open>Subspaces\<close> |
5 section \<open>Subspaces\<close> |
6 |
6 |
7 theory Subspace |
7 theory Subspace |
8 imports Vector_Space "~~/src/HOL/Library/Set_Algebras" |
8 imports Vector_Space "HOL-Library.Set_Algebras" |
9 begin |
9 begin |
10 |
10 |
11 subsection \<open>Definition\<close> |
11 subsection \<open>Definition\<close> |
12 |
12 |
13 text \<open> |
13 text \<open> |