src/HOL/Multivariate_Analysis/Path_Connected.thy
changeset 63126 2b50f79829d2
parent 63125 f2d3f8427bc2
child 63151 82df5181d699
equal deleted inserted replaced
63125:f2d3f8427bc2 63126:2b50f79829d2
  5250 by (metis Compl_eq_Diff_UNIV S c closed_closedin closedin_Un_complement_component locally_connected_UNIV subtopology_UNIV)
  5250 by (metis Compl_eq_Diff_UNIV S c closed_closedin closedin_Un_complement_component locally_connected_UNIV subtopology_UNIV)
  5251 
  5251 
  5252 
  5252 
  5253 subsection\<open>Existence of isometry between subspaces of same dimension\<close>
  5253 subsection\<open>Existence of isometry between subspaces of same dimension\<close>
  5254 
  5254 
  5255 thm subspace_isomorphism
       
  5256 lemma isometry_subset_subspace:
  5255 lemma isometry_subset_subspace:
  5257   fixes S :: "'a::euclidean_space set"
  5256   fixes S :: "'a::euclidean_space set"
  5258     and T :: "'b::euclidean_space set"
  5257     and T :: "'b::euclidean_space set"
  5259   assumes S: "subspace S"
  5258   assumes S: "subspace S"
  5260       and T: "subspace T"
  5259       and T: "subspace T"