equal
deleted
inserted
replaced
5410 apply (rule that [OF \<open>linear f\<close> \<open>linear g\<close>]) |
5410 apply (rule that [OF \<open>linear f\<close> \<open>linear g\<close>]) |
5411 apply (simp_all add: fim gim) |
5411 apply (simp_all add: fim gim) |
5412 done |
5412 done |
5413 qed |
5413 qed |
5414 |
5414 |
5415 (*REPLACE*) |
|
5416 lemma isometry_subspaces: |
5415 lemma isometry_subspaces: |
5417 fixes S :: "'a::euclidean_space set" |
5416 fixes S :: "'a::euclidean_space set" |
5418 and T :: "'b::euclidean_space set" |
5417 and T :: "'b::euclidean_space set" |
5419 assumes S: "subspace S" |
5418 assumes S: "subspace S" |
5420 and T: "subspace T" |
5419 and T: "subspace T" |