equal
deleted
inserted
replaced
5 prove: b \<in> Fin(A) ==> inj(b,b) \<subseteq> surj(b,b) |
5 prove: b \<in> Fin(A) ==> inj(b,b) \<subseteq> surj(b,b) |
6 *) |
6 *) |
7 |
7 |
8 section\<open>Finite Powerset Operator and Finite Function Space\<close> |
8 section\<open>Finite Powerset Operator and Finite Function Space\<close> |
9 |
9 |
10 theory Finite imports Inductive_ZF Epsilon Nat_ZF begin |
10 theory Finite imports Inductive Epsilon Nat begin |
11 |
11 |
12 (*The natural numbers as a datatype*) |
12 (*The natural numbers as a datatype*) |
13 rep_datatype |
13 rep_datatype |
14 elimination natE |
14 elimination natE |
15 induction nat_induct |
15 induction nat_induct |