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/set.mg | |
| parent | 9d34eebafc87e6bce476ccc487a88b440315089b (diff) | |
Update lemma name
Diffstat (limited to 'megalodon/library/set.mg')
| -rw-r--r-- | megalodon/library/set.mg | 2 |
1 files changed, 1 insertions, 1 deletions
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)). |