1283 proof (rule partial_order.complete_latticeI) |
1283 proof (rule partial_order.complete_latticeI) |
1284 show "partial_order ?L" |
1284 show "partial_order ?L" |
1285 by default auto |
1285 by default auto |
1286 next |
1286 next |
1287 fix B |
1287 fix B |
1288 assume B: "B \<subseteq> carrier ?L" |
1288 assume "B \<subseteq> carrier ?L" |
1289 show "EX s. least ?L s (Upper ?L B)" |
1289 then have "least ?L (\<Union> B) (Upper ?L B)" |
1290 proof |
1290 by (fastforce intro!: least_UpperI simp: Upper_def) |
1291 from B show "least ?L (\<Union> B) (Upper ?L B)" |
1291 then show "EX s. least ?L s (Upper ?L B)" .. |
1292 by (fastforce intro!: least_UpperI simp: Upper_def) |
|
1293 qed |
|
1294 next |
1292 next |
1295 fix B |
1293 fix B |
1296 assume B: "B \<subseteq> carrier ?L" |
1294 assume "B \<subseteq> carrier ?L" |
1297 show "EX i. greatest ?L i (Lower ?L B)" |
1295 then have "greatest ?L (\<Inter> B \<inter> A) (Lower ?L B)" |
1298 proof |
1296 txt {* @{term "\<Inter> B"} is not the infimum of @{term B}: |
1299 from B show "greatest ?L (\<Inter> B \<inter> A) (Lower ?L B)" |
1297 @{term "\<Inter> {} = UNIV"} which is in general bigger than @{term "A"}! *} |
1300 txt {* @{term "\<Inter> B"} is not the infimum of @{term B}: |
1298 by (fastforce intro!: greatest_LowerI simp: Lower_def) |
1301 @{term "\<Inter> {} = UNIV"} which is in general bigger than @{term "A"}! *} |
1299 then show "EX i. greatest ?L i (Lower ?L B)" .. |
1302 by (fastforce intro!: greatest_LowerI simp: Lower_def) |
|
1303 qed |
|
1304 qed |
1300 qed |
1305 |
1301 |
1306 text {* An other example, that of the lattice of subgroups of a group, |
1302 text {* An other example, that of the lattice of subgroups of a group, |
1307 can be found in Group theory (Section~\ref{sec:subgroup-lattice}). *} |
1303 can be found in Group theory (Section~\ref{sec:subgroup-lattice}). *} |
1308 |
1304 |