equal
deleted
inserted
replaced
293 by (rule finite_range_cfun_map) |
293 by (rule finite_range_cfun_map) |
294 thus "finite {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}" |
294 thus "finite {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}" |
295 by (rule finite_range_imp_finite_fixes) |
295 by (rule finite_range_imp_finite_fixes) |
296 qed |
296 qed |
297 |
297 |
|
298 text {* Finite deflations are compact elements of the function space *} |
|
299 |
|
300 lemma finite_deflation_imp_compact: "finite_deflation d \<Longrightarrow> compact d" |
|
301 apply (frule finite_deflation_imp_deflation) |
|
302 apply (subgoal_tac "compact (cfun_map\<cdot>d\<cdot>d\<cdot>d)") |
|
303 apply (simp add: cfun_map_def deflation.idem eta_cfun) |
|
304 apply (rule finite_deflation.compact) |
|
305 apply (simp only: finite_deflation_cfun_map) |
|
306 done |
|
307 |
298 instantiation cfun :: (profinite, profinite) profinite |
308 instantiation cfun :: (profinite, profinite) profinite |
299 begin |
309 begin |
300 |
310 |
301 definition |
311 definition |
302 approx_cfun_def: |
312 approx_cfun_def: |