diff options
| author | adelon <22380201+adelon@users.noreply.github.com> | 2025-07-08 22:16:01 +0200 |
|---|---|---|
| committer | adelon <22380201+adelon@users.noreply.github.com> | 2025-07-08 22:16:01 +0200 |
| commit | da6d425281534407a92ce18a22584905a7847a39 (patch) | |
| tree | 2449971b42b96b566039e0c2c9a575481ae51f38 /megalodon/library | |
| parent | 9d34eebafc87e6bce476ccc487a88b440315089b (diff) | |
Update lemma name
Diffstat (limited to 'megalodon/library')
| -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)). |