equal
deleted
inserted
replaced
17 (* ========================================================================= *) |
17 (* ========================================================================= *) |
18 |
18 |
19 section \<open>Results connected with topological dimension.\<close> |
19 section \<open>Results connected with topological dimension.\<close> |
20 |
20 |
21 theory Brouwer_Fixpoint |
21 theory Brouwer_Fixpoint |
22 imports Path_Connected |
22 imports Path_Connected Homeomorphism |
23 begin |
23 begin |
24 |
24 |
25 lemma bij_betw_singleton_eq: |
25 lemma bij_betw_singleton_eq: |
26 assumes f: "bij_betw f A B" and g: "bij_betw g A B" and a: "a \<in> A" |
26 assumes f: "bij_betw f A B" and g: "bij_betw g A B" and a: "a \<in> A" |
27 assumes eq: "(\<And>x. x \<in> A \<Longrightarrow> x \<noteq> a \<Longrightarrow> f x = g x)" |
27 assumes eq: "(\<And>x. x \<in> A \<Longrightarrow> x \<noteq> a \<Longrightarrow> f x = g x)" |