src/HOL/Multivariate_Analysis/Path_Connected.thy
changeset 63125 f2d3f8427bc2
parent 63114 27afe7af7379
child 63126 2b50f79829d2
equal deleted inserted replaced
63115:39dca4891601 63125:f2d3f8427bc2
  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"