equal
deleted
inserted
replaced
1062 qed |
1062 qed |
1063 |
1063 |
1064 lemma relpow_finite_bounded: |
1064 lemma relpow_finite_bounded: |
1065 fixes R :: "('a \<times> 'a) set" |
1065 fixes R :: "('a \<times> 'a) set" |
1066 assumes "finite R" |
1066 assumes "finite R" |
1067 shows "R^^k \<subseteq> (UN n:{n. n \<le> card R}. R^^n)" |
1067 shows "R^^k \<subseteq> (\<Union>n\<in>{n. n \<le> card R}. R^^n)" |
1068 apply (cases k, force) |
1068 apply (cases k, force) |
1069 apply (use relpow_finite_bounded1[OF assms, of k] in auto) |
1069 apply (use relpow_finite_bounded1[OF assms, of k] in auto) |
1070 done |
1070 done |
1071 |
1071 |
1072 lemma rtrancl_finite_eq_relpow: "finite R \<Longrightarrow> R\<^sup>* = (\<Union>n\<in>{n. n \<le> card R}. R^^n)" |
1072 lemma rtrancl_finite_eq_relpow: "finite R \<Longrightarrow> R\<^sup>* = (\<Union>n\<in>{n. n \<le> card R}. R^^n)" |