equal
deleted
inserted
replaced
49 lemma card_of_Times_singleton: |
49 lemma card_of_Times_singleton: |
50 fixes A :: "'a set" |
50 fixes A :: "'a set" |
51 shows "|A \<times> {x}| =o |A|" |
51 shows "|A \<times> {x}| =o |A|" |
52 proof - |
52 proof - |
53 def f \<equiv> "\<lambda>(a::'a,b::'b). (a)" |
53 def f \<equiv> "\<lambda>(a::'a,b::'b). (a)" |
54 have "A \<subseteq> f ` (A <*> {x})" unfolding f_def by (auto simp: image_iff) |
54 have "A \<subseteq> f ` (A \<times> {x})" unfolding f_def by (auto simp: image_iff) |
55 hence "bij_betw f (A <*> {x}) A" unfolding bij_betw_def inj_on_def f_def by fastforce |
55 hence "bij_betw f (A \<times> {x}) A" unfolding bij_betw_def inj_on_def f_def by fastforce |
56 thus ?thesis using card_of_ordIso by blast |
56 thus ?thesis using card_of_ordIso by blast |
57 qed |
57 qed |
58 |
58 |
59 lemma cprod_assoc: "(r *c s) *c t =o r *c s *c t" |
59 lemma cprod_assoc: "(r *c s) *c t =o r *c s *c t" |
60 unfolding cprod_def Field_card_of by (rule card_of_Times_assoc) |
60 unfolding cprod_def Field_card_of by (rule card_of_Times_assoc) |