src/HOL/Cardinals/Cardinal_Order_Relation.thy
 changeset 54989 0fd6b0660242 parent 54980 7e0573a490ee child 55023 38db7814481d
equal inserted replaced
54988:f3b6f80cc15d 54989:0fd6b0660242
`  1852 lemma stable_nat: "stable |UNIV::nat set|"`
`  1852 lemma stable_nat: "stable |UNIV::nat set|"`
`  1853 using stable_natLeq card_of_nat stable_ordIso by auto`
`  1853 using stable_natLeq card_of_nat stable_ordIso by auto`
`  1854 `
`  1854 `
`  1855 text{* Below, the type of "A" is not important -- we just had to choose an appropriate`
`  1855 text{* Below, the type of "A" is not important -- we just had to choose an appropriate`
`  1856    type to make "A" possible. What is important is that arbitrarily large`
`  1856    type to make "A" possible. What is important is that arbitrarily large`
`  1857    \<not>finite sets of stable cardinality exist. *}`
`  1857    infinite sets of stable cardinality exist. *}`
`  1858 `
`  1858 `
`  1859 lemma infinite_stable_exists:`
`  1859 lemma infinite_stable_exists:`
`  1860 assumes CARD: "\<forall>r \<in> R. Card_order (r::'a rel)"`
`  1860 assumes CARD: "\<forall>r \<in> R. Card_order (r::'a rel)"`
`  1861 shows "\<exists>(A :: (nat + 'a set)set).`
`  1861 shows "\<exists>(A :: (nat + 'a set)set).`
`  1862           \<not>finite A \<and> stable |A| \<and> (\<forall>r \<in> R. r <o |A| )"`
`  1862           \<not>finite A \<and> stable |A| \<and> (\<forall>r \<in> R. r <o |A| )"`