equal
deleted
inserted
replaced
1150 by (auto simp add: Powp_def fun_eq_iff) |
1150 by (auto simp add: Powp_def fun_eq_iff) |
1151 |
1151 |
1152 lemmas Powp_mono [mono] = Pow_mono [to_pred] |
1152 lemmas Powp_mono [mono] = Pow_mono [to_pred] |
1153 |
1153 |
1154 |
1154 |
1155 subsubsection \<open>Expressing relation operations via @{const Finite_Set.fold}\<close> |
1155 subsubsection \<open>Expressing relation operations via \<^const>\<open>Finite_Set.fold\<close>\<close> |
1156 |
1156 |
1157 lemma Id_on_fold: |
1157 lemma Id_on_fold: |
1158 assumes "finite A" |
1158 assumes "finite A" |
1159 shows "Id_on A = Finite_Set.fold (\<lambda>x. Set.insert (Pair x x)) {} A" |
1159 shows "Id_on A = Finite_Set.fold (\<lambda>x. Set.insert (Pair x x)) {} A" |
1160 proof - |
1160 proof - |