equal
deleted
inserted
replaced
22 the function @{text f} and let @{text "graph H h"} be the supremum |
22 the function @{text f} and let @{text "graph H h"} be the supremum |
23 of @{text c}. Every element in @{text H} is member of one of the |
23 of @{text c}. Every element in @{text H} is member of one of the |
24 elements of the chain. |
24 elements of the chain. |
25 *} |
25 *} |
26 lemmas [dest?] = chainD |
26 lemmas [dest?] = chainD |
27 lemmas chainE2 [elim?] = chainD2 [elim_format, standard] |
27 lemmas chainE2 [elim?] = chainD2 [elim_format] |
28 |
28 |
29 lemma some_H'h't: |
29 lemma some_H'h't: |
30 assumes M: "M = norm_pres_extensions E p F f" |
30 assumes M: "M = norm_pres_extensions E p F f" |
31 and cM: "c \<in> chain M" |
31 and cM: "c \<in> chain M" |
32 and u: "graph H h = \<Union>c" |
32 and u: "graph H h = \<Union>c" |