diff options
Diffstat (limited to 'megalodon')
| -rw-r--r-- | megalodon/library/cardinal.mg | 2 | ||||
| -rw-r--r-- | megalodon/library/relation/equivalence.mg | 2 | ||||
| -rw-r--r-- | megalodon/library/set.mg | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/megalodon/library/cardinal.mg b/megalodon/library/cardinal.mg index 4d2af41..19991b2 100644 --- a/megalodon/library/cardinal.mg +++ b/megalodon/library/cardinal.mg @@ -36,7 +36,7 @@ Admitted. Theorem subset_witness : (forall A B,(((subset A B)->(exists b,(((elem b B)/\(notelem b A))))))). Admitted. Definition family_of_subsets := fun x0 x1 : set => (forall A,(((elem A x0)->(subseteq A x1)))). -Fact notin_emptyset : (forall a,((notelem a (emptyset)))). +Fact emptyset : (forall a,((notelem a (emptyset)))). Admitted. Definition inhabited := fun A: set => (exists a,((elem a A))). Definition empty := fun x0 : set => ~((inhabited x0)). diff --git a/megalodon/library/relation/equivalence.mg b/megalodon/library/relation/equivalence.mg index e9c8211..cc93394 100644 --- a/megalodon/library/relation/equivalence.mg +++ b/megalodon/library/relation/equivalence.mg @@ -35,7 +35,7 @@ Admitted. Theorem subset_witness : (forall A B,(((subset A B)->(exists b,(((elem b B)/\(notelem b A))))))). Admitted. Definition family_of_subsets := fun x0 x1 : set => (forall A,(((elem A x0)->(subseteq A x1)))). -Fact notin_emptyset : (forall a,((notelem a (emptyset)))). +Fact emptyset : (forall a,((notelem a (emptyset)))). Admitted. Definition inhabited := fun A: set => (exists a,((elem a A))). Definition empty := fun x0 : set => ~((inhabited x0)). diff --git a/megalodon/library/set.mg b/megalodon/library/set.mg index 3606b4e..7c86a69 100644 --- a/megalodon/library/set.mg +++ b/megalodon/library/set.mg @@ -36,7 +36,7 @@ Admitted. Theorem subset_witness : (forall A B,(((subset A B)->(exists b,(((elem b B)/\(notelem b A))))))). Admitted. Definition family_of_subsets := fun x0 x1 : set => (forall A,(((elem A x0)->(subseteq A x1)))). -Fact notin_emptyset : (forall a,((notelem a (emptyset)))). +Fact emptyset : (forall a,((notelem a (emptyset)))). Admitted. Definition inhabited := fun A: set => (exists a,((elem a A))). Definition empty := fun x0 : set => ~((inhabited x0)). |