equal
deleted
inserted
replaced
434 dualA_iff[simp del] |
434 dualA_iff[simp del] |
435 |
435 |
436 subsection \<open>fixed points\<close> |
436 subsection \<open>fixed points\<close> |
437 |
437 |
438 lemma fix_subset: "fix f A \<subseteq> A" |
438 lemma fix_subset: "fix f A \<subseteq> A" |
439 by (simp add: fix_def, fast) |
439 by (auto simp add: fix_def) |
440 |
440 |
441 lemma fix_imp_eq: "x \<in> fix f A ==> f x = x" |
441 lemma fix_imp_eq: "x \<in> fix f A ==> f x = x" |
442 by (simp add: fix_def) |
442 by (simp add: fix_def) |
443 |
443 |
444 lemma fixf_subset: |
444 lemma fixf_subset: |