src/HOL/Cardinals/Cardinal_Order_Relation.thy
changeset 54989 0fd6b0660242
parent 54980 7e0573a490ee
child 55023 38db7814481d
equal deleted 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| )"