equal
deleted
inserted
replaced
3 Author: Gertrud Bauer, TU Munich |
3 Author: Gertrud Bauer, TU Munich |
4 *) |
4 *) |
5 |
5 |
6 header {* Zorn's Lemma *} |
6 header {* Zorn's Lemma *} |
7 |
7 |
8 theory ZornLemma = Zorn: |
8 theory ZornLemma imports Zorn begin |
9 |
9 |
10 text {* |
10 text {* |
11 Zorn's Lemmas states: if every linear ordered subset of an ordered |
11 Zorn's Lemmas states: if every linear ordered subset of an ordered |
12 set @{text S} has an upper bound in @{text S}, then there exists a |
12 set @{text S} has an upper bound in @{text S}, then there exists a |
13 maximal element in @{text S}. In our application, @{text S} is a |
13 maximal element in @{text S}. In our application, @{text S} is a |