equal
deleted
inserted
replaced
541 qed |
541 qed |
542 |
542 |
543 end |
543 end |
544 |
544 |
545 |
545 |
546 subsection \<open>Complete lattices where @{text eq} is the Equality\<close> |
546 subsection \<open>Complete lattices where \<open>eq\<close> is the Equality\<close> |
547 |
547 |
548 locale complete_lattice = partial_order + |
548 locale complete_lattice = partial_order + |
549 assumes sup_exists: |
549 assumes sup_exists: |
550 "[| A \<subseteq> carrier L |] ==> \<exists>s. least L s (Upper L A)" |
550 "[| A \<subseteq> carrier L |] ==> \<exists>s. least L s (Upper L A)" |
551 and inf_exists: |
551 and inf_exists: |