Update lemma name

7 files changed, 12 insertions, 12 deletions

diff --git a/library/function.tex b/library/function.tex
index 47d399f..7616593 100644
--- a/library/function.tex
+++ b/library/function.tex
@@ -465,7 +465,7 @@
     Then $f(x) = \emptyset$.
 \end{proposition}
 \begin{proof}
-    $\img{f}{\{x\}} = \emptyset$ by \cref{setext,notin_emptyset,img_singleton_iff,dom_intro}.
+    $\img{f}{\{x\}} = \emptyset$ by \cref{setext,emptyset,img_singleton_iff,dom_intro}.
     Follows by \cref{apply,unions_emptyset}.
 \end{proof}
 
diff --git a/library/ordinal.tex b/library/ordinal.tex
index 6f924c1..c092fa8 100644
--- a/library/ordinal.tex
+++ b/library/ordinal.tex
@@ -559,7 +559,7 @@ Then $\alpha\subseteq\beta$.
 \end{lemma}
 \begin{proof}
     Suppose not.
-    Then $\emptyset\precedes \emptyset$ by \cref{notin_emptyset,limit_ordinal}.
+    Then $\emptyset\precedes \emptyset$ by \cref{emptyset,limit_ordinal}.
     Thus $\emptyset\in \emptyset$.
     Contradiction.
 \end{proof}
@@ -636,4 +636,4 @@ Then $\alpha\subseteq\beta$.
 %    $\emptyset\precedes \naturals$.
 %    If $n\in \naturals$, then $\suc{n}\in\naturals$.
 %\end{proof}
-%
\ No newline at end of file
+%
diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex
index bfbf54d..22508e1 100644
--- a/library/topology/urysohn.tex
+++ b/library/topology/urysohn.tex
@@ -752,8 +752,8 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct.
 %
 %            Omitted.
 %
-%            % Contradiction by \cref{two_in_naturals,function_apply_default,reals_axiom_zero_in_reals,dom_emptyset,notin_emptyset,funs_type_apply,neg,minus,abs_behavior1}.
-%            %Follows by \cref{two_in_naturals,function_apply_default,reals_axiom_zero_in_reals,dom_emptyset,notin_emptyset,funs_type_apply,neg,minus,abs_behavior1}.
+%            % Contradiction by \cref{two_in_naturals,function_apply_default,reals_axiom_zero_in_reals,dom_emptyset,emptyset,funs_type_apply,neg,minus,abs_behavior1}.
+%            %Follows by \cref{two_in_naturals,function_apply_default,reals_axiom_zero_in_reals,dom_emptyset,emptyset,funs_type_apply,neg,minus,abs_behavior1}.
 %        \end{subproof}
 %        Omitted.
 %    \end{subproof}
diff --git a/library/topology/urysohntwo.tex b/library/topology/urysohntwo.tex
index 68faeac..eda3c32 100644
--- a/library/topology/urysohntwo.tex
+++ b/library/topology/urysohntwo.tex
@@ -164,7 +164,7 @@
     There exists no $x$ such that $x \in \zero$.
 \end{proposition}
 \begin{proof}
-    Follows by \cref{notin_emptyset}.
+    Follows by \cref{emptyset}.
 \end{proof}
 
 \begin{proposition}\label{one_is_positiv}
@@ -473,7 +473,7 @@
 \begin{proof}[Proof by \in-induction on $n$]
     Assume $n \in \naturals$.
     Suppose $Y$ has cardinality $n$.
-    $X$ has cardinality $n$ by \cref{bijection_converse_is_bijection,bijection_circ,regularity,cardinality,foundation,empty_eq,notin_emptyset}.
+    $X$ has cardinality $n$ by \cref{bijection_converse_is_bijection,bijection_circ,regularity,cardinality,foundation,empty_eq,emptyset}.
     \begin{byCase}
         \caseOf{$n = \zero$.}
             Follows by \cref{converse_converse_eq,injective_converse_is_function,converse_is_relation,dom_converse,id_is_function_to,id_ran,ran_circ_exact,circ,ran_converse,emptyset_is_function_on_emptyset,bijective_converse_are_funs,relext,function_member_elim,bijection_is_function,cardinality,bijections_dom,in_irrefl,codom_of_emptyset_can_be_anything,converse_emptyset,funs_elim,neq_witness,id}.
@@ -817,7 +817,7 @@
                         We have $A \subseteq A'$.
                         We have $\at{U_0}{\zero} = A$ by assumption.
                         We have $\at{U_0}{1}= A'$ by assumption.
-                        Follows by \cref{powerset_elim,emptyset_subseteq,union_as_unions,union_absorb_subseteq_left,subseteq_pow_unions,ran_converse,subseteq,subseteq_antisymmetric,suc_subseteq_intro,apply,powerset_emptyset,emptyset_is_ordinal,notin_emptyset,ordinal_elem_connex,omega_is_an_ordinal,prec_is_ordinal}.
+                        Follows by \cref{powerset_elim,emptyset_subseteq,union_as_unions,union_absorb_subseteq_left,subseteq_pow_unions,ran_converse,subseteq,subseteq_antisymmetric,suc_subseteq_intro,apply,powerset_emptyset,emptyset_is_ordinal,emptyset,ordinal_elem_connex,omega_is_an_ordinal,prec_is_ordinal}.
                 \end{byCase}
         \end{byCase}
     \end{subproof}
@@ -835,7 +835,7 @@
                     \caseOf{$m = \zero$.}
                         Trivial.
                     \caseOf{$m \neq \zero$.}
-                        Follows by \cref{setminus_emptyset,setdifference_eq_intersection_with_complement,setminus_self,interior_carrier,complement_interior_eq_closure_complement,subseteq_refl,closure_interior_frontier_is_in_carrier,emptyset_subseteq,closure_is_minimal_closed_set,inter_lower_right,inter_lower_left,subseteq_transitive,interior_of_open,is_closed_in,closeds,union_absorb_subseteq_right,ordinal_suc_subseteq,ordinal_empty_or_emptyset_elem,union_absorb_subseteq_left,union_emptyset,topological_prebasis_iff_covering_family,notin_emptyset,subseteq,union_as_unions,natural_number_is_ordinal}.
+                        Follows by \cref{setminus_emptyset,setdifference_eq_intersection_with_complement,setminus_self,interior_carrier,complement_interior_eq_closure_complement,subseteq_refl,closure_interior_frontier_is_in_carrier,emptyset_subseteq,closure_is_minimal_closed_set,inter_lower_right,inter_lower_left,subseteq_transitive,interior_of_open,is_closed_in,closeds,union_absorb_subseteq_right,ordinal_suc_subseteq,ordinal_empty_or_emptyset_elem,union_absorb_subseteq_left,union_emptyset,topological_prebasis_iff_covering_family,emptyset,subseteq,union_as_unions,natural_number_is_ordinal}.
                 \end{byCase}
         \end{byCase}
     \end{subproof}
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)).