src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
 changeset 37452 8f515d6aded5 parent 36778 739a9379e29b child 37486 b993fac7985b child 37489 44e42d392c6e
equal inserted replaced
`  5264 lemma homeomorphic_compact:`
`  5264 lemma homeomorphic_compact:`
`  5265   fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel"`
`  5265   fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel"`
`  5266     (* class constraint due to continuous_on_inverse *)`
`  5266     (* class constraint due to continuous_on_inverse *)`
`  5267   shows "compact s \<Longrightarrow> continuous_on s f \<Longrightarrow> (f ` s = t) \<Longrightarrow> inj_on f s`
`  5267   shows "compact s \<Longrightarrow> continuous_on s f \<Longrightarrow> (f ` s = t) \<Longrightarrow> inj_on f s`
`  5268           \<Longrightarrow> s homeomorphic t"`
`  5268           \<Longrightarrow> s homeomorphic t"`
`  5269   unfolding homeomorphic_def by(metis homeomorphism_compact)`
`  5269   unfolding homeomorphic_def by (auto intro: homeomorphism_compact)`
`  5270 `
`  5270 `
`  5271 text{* Preservation of topological properties.                                   *}`
`  5271 text{* Preservation of topological properties.                                   *}`
`  5272 `
`  5272 `
`  5273 lemma homeomorphic_compactness:`
`  5273 lemma homeomorphic_compactness:`
`  5274  "s homeomorphic t ==> (compact s \<longleftrightarrow> compact t)"`
`  5274  "s homeomorphic t ==> (compact s \<longleftrightarrow> compact t)"`