summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

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| )" |