equal
deleted
inserted
replaced
31 lemma finite_range_approx: "finite (range (\<lambda>x. approx i\<cdot>x))" |
31 lemma finite_range_approx: "finite (range (\<lambda>x. approx i\<cdot>x))" |
32 apply (rule finite_deflation.finite_range) |
32 apply (rule finite_deflation.finite_range) |
33 apply (rule finite_deflation_approx) |
33 apply (rule finite_deflation_approx) |
34 done |
34 done |
35 |
35 |
36 lemma compact_approx: "compact (approx n\<cdot>x)" |
36 lemma compact_approx [simp]: "compact (approx n\<cdot>x)" |
37 apply (rule finite_deflation.compact) |
37 apply (rule finite_deflation.compact) |
38 apply (rule finite_deflation_approx) |
38 apply (rule finite_deflation_approx) |
39 done |
39 done |
40 |
40 |
41 lemma compact_eq_approx: "compact x \<Longrightarrow> \<exists>i. approx i\<cdot>x = x" |
41 lemma compact_eq_approx: "compact x \<Longrightarrow> \<exists>i. approx i\<cdot>x = x" |