equal
deleted
inserted
replaced
5282 lemma homeomorphic_compact: |
5282 lemma homeomorphic_compact: |
5283 fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel" |
5283 fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel" |
5284 (* class constraint due to continuous_on_inverse *) |
5284 (* class constraint due to continuous_on_inverse *) |
5285 shows "compact s \<Longrightarrow> continuous_on s f \<Longrightarrow> (f ` s = t) \<Longrightarrow> inj_on f s |
5285 shows "compact s \<Longrightarrow> continuous_on s f \<Longrightarrow> (f ` s = t) \<Longrightarrow> inj_on f s |
5286 \<Longrightarrow> s homeomorphic t" |
5286 \<Longrightarrow> s homeomorphic t" |
5287 unfolding homeomorphic_def by(auto intro: homeomorphism_compact) |
5287 unfolding homeomorphic_def by (metis homeomorphism_compact) |
5288 |
5288 |
5289 text{* Preservation of topological properties. *} |
5289 text{* Preservation of topological properties. *} |
5290 |
5290 |
5291 lemma homeomorphic_compactness: |
5291 lemma homeomorphic_compactness: |
5292 "s homeomorphic t ==> (compact s \<longleftrightarrow> compact t)" |
5292 "s homeomorphic t ==> (compact s \<longleftrightarrow> compact t)" |