equal
deleted
inserted
replaced
414 (* FIXME: long proof! *) |
414 (* FIXME: long proof! *) |
415 lemma finite_deflation_upper_map: |
415 lemma finite_deflation_upper_map: |
416 assumes "finite_deflation d" shows "finite_deflation (upper_map\<cdot>d)" |
416 assumes "finite_deflation d" shows "finite_deflation (upper_map\<cdot>d)" |
417 proof (rule finite_deflation_intro) |
417 proof (rule finite_deflation_intro) |
418 interpret d: finite_deflation d by fact |
418 interpret d: finite_deflation d by fact |
419 have "deflation d" by fact |
419 from d.deflation_axioms show "deflation (upper_map\<cdot>d)" |
420 thus "deflation (upper_map\<cdot>d)" by (rule deflation_upper_map) |
420 by (rule deflation_upper_map) |
421 have "finite (range (\<lambda>x. d\<cdot>x))" by (rule d.finite_range) |
421 have "finite (range (\<lambda>x. d\<cdot>x))" by (rule d.finite_range) |
422 hence "finite (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))" |
422 hence "finite (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))" |
423 by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject) |
423 by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject) |
424 hence "finite (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x)))" by simp |
424 hence "finite (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x)))" by simp |
425 hence "finite (Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))))" |
425 hence "finite (Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))))" |