equal
deleted
inserted
replaced
1 section\<open>Invariance of Domain\<close> |
1 section\<open>Invariance of Domain\<close> |
2 |
2 |
3 theory Invariance_of_Domain |
3 theory Invariance_of_Domain |
4 imports Brouwer_Degree "HOL-Analysis.Continuous_Extension" "HOL-Analysis.Homeomorphism" |
4 imports Brouwer_Degree "HOL-Analysis.Continuous_Extension" "HOL-Analysis.Homeomorphism" |
5 |
5 |
6 begin |
6 begin |
7 |
7 |
8 subsection\<open>Degree invariance mod 2 for map between pairs\<close> |
8 subsection\<open>Degree invariance mod 2 for map between pairs\<close> |
9 |
9 |
2063 by (simp add: inf_commute) |
2063 by (simp add: inf_commute) |
2064 qed |
2064 qed |
2065 qed |
2065 qed |
2066 |
2066 |
2067 |
2067 |
2068 |
2068 subsection\<open> Invariance of dimension and domain\<close> |
2069 subsection\<open> Invariance of dimension and domain in setting of R^n.\<close> |
|
2070 |
2069 |
2071 lemma homeomorphic_maps_iff_homeomorphism [simp]: |
2070 lemma homeomorphic_maps_iff_homeomorphism [simp]: |
2072 "homeomorphic_maps (top_of_set S) (top_of_set T) f g \<longleftrightarrow> homeomorphism S T f g" |
2071 "homeomorphic_maps (top_of_set S) (top_of_set T) f g \<longleftrightarrow> homeomorphism S T f g" |
2073 unfolding homeomorphic_maps_def homeomorphism_def by force |
2072 unfolding homeomorphic_maps_def homeomorphism_def by force |
2074 |
2073 |