equal
deleted
inserted
replaced
82 then show "\<exists>f::nat\<Rightarrow>atom. inj f \<and> range f \<subseteq> ODD" by (rule_tac exI) |
82 then show "\<exists>f::nat\<Rightarrow>atom. inj f \<and> range f \<subseteq> ODD" by (rule_tac exI) |
83 qed |
83 qed |
84 |
84 |
85 text {* |
85 text {* |
86 A general fact about a set S of atoms that is both infinite and |
86 A general fact about a set S of atoms that is both infinite and |
87 coinfinite. Then S has all atoms as its support. Steve Zdancewick |
87 coinfinite. Then S has all atoms as its support. Steve Zdancewic |
88 helped with proving this fact. *} |
88 helped with proving this fact. *} |
89 |
89 |
90 lemma supp_infinite_coinfinite: |
90 lemma supp_infinite_coinfinite: |
91 fixes S::"atom set" |
91 fixes S::"atom set" |
92 assumes asm1: "infinite S" |
92 assumes asm1: "infinite S" |