diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/topology/urysohntwo.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/topology/urysohntwo.tex b/library/topology/urysohntwo.tex index eda3c32..7f69aa4 100644 --- a/library/topology/urysohntwo.tex +++ b/library/topology/urysohntwo.tex @@ -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,emptyset}. + $X$ has cardinality $n$ by \cref{bijection_converse_is_bijection,bijection_circ,regularity,cardinality,foundation,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}. |