equal
deleted
inserted
replaced
1 (* Title: ZF/Cardinal.thy |
1 (* Title: ZF/Cardinal.thy |
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1994 University of Cambridge |
3 Copyright 1994 University of Cambridge |
5 |
|
6 *) |
4 *) |
7 |
5 |
8 header{*Cardinal Numbers Without the Axiom of Choice*} |
6 header{*Cardinal Numbers Without the Axiom of Choice*} |
9 |
7 |
10 theory Cardinal imports OrderType Finite Nat_ZF Sum begin |
8 theory Cardinal imports OrderType Finite Nat_ZF Sum begin |
58 by (rule bnd_monoI, blast+) |
56 by (rule bnd_monoI, blast+) |
59 |
57 |
60 lemma Banach_last_equation: |
58 lemma Banach_last_equation: |
61 "g: Y->X |
59 "g: Y->X |
62 ==> g``(Y - f`` lfp(X, %W. X - g``(Y - f``W))) = |
60 ==> g``(Y - f`` lfp(X, %W. X - g``(Y - f``W))) = |
63 X - lfp(X, %W. X - g``(Y - f``W))" |
61 X - lfp(X, %W. X - g``(Y - f``W))" |
64 apply (rule_tac P = "%u. ?v = X-u" |
62 apply (rule_tac P = "%u. ?v = X-u" |
65 in decomp_bnd_mono [THEN lfp_unfold, THEN ssubst]) |
63 in decomp_bnd_mono [THEN lfp_unfold, THEN ssubst]) |
66 apply (simp add: double_complement fun_is_rel [THEN image_subset]) |
64 apply (simp add: double_complement fun_is_rel [THEN image_subset]) |
67 done |
65 done |
68 |
66 |