diff options
Diffstat (limited to 'megalodon/library/relation/equivalence.mg')
| -rw-r--r-- | megalodon/library/relation/equivalence.mg | 2 |
1 files changed, 1 insertions, 1 deletions
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)). |