equal
deleted
inserted
replaced
444 apply (rule finite_imageD [where f="\<lambda>a. {x. Rep_fin_defl a\<cdot>x = x}"]) |
444 apply (rule finite_imageD [where f="\<lambda>a. {x. Rep_fin_defl a\<cdot>x = x}"]) |
445 apply (rule finite_subset [where B="Pow {x. approx n\<cdot>x = x}"]) |
445 apply (rule finite_subset [where B="Pow {x. approx n\<cdot>x = x}"]) |
446 apply (clarify, simp add: fd_take_fixed_iff) |
446 apply (clarify, simp add: fd_take_fixed_iff) |
447 apply (simp add: finite_fixes_approx) |
447 apply (simp add: finite_fixes_approx) |
448 apply (rule inj_onI, clarify) |
448 apply (rule inj_onI, clarify) |
449 apply (simp add: set_ext_iff fin_defl_eqI) |
449 apply (simp add: set_eq_iff fin_defl_eqI) |
450 done |
450 done |
451 |
451 |
452 lemma fd_take_covers: "\<exists>n. fd_take n a = a" |
452 lemma fd_take_covers: "\<exists>n. fd_take n a = a" |
453 apply (rule_tac x= |
453 apply (rule_tac x= |
454 "Max ((\<lambda>x. LEAST n. approx n\<cdot>x = x) ` {x. Rep_fin_defl a\<cdot>x = x})" in exI) |
454 "Max ((\<lambda>x. LEAST n. approx n\<cdot>x = x) ` {x. Rep_fin_defl a\<cdot>x = x})" in exI) |