From 39ef87d3ce39152febc130aa95e25dc0722c3525 Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Tue, 12 Aug 2025 00:37:28 +0200
Subject: Allow relation symbols with parameters

Parameters must follow the relation symbol and be surrounded by braces, like so: `\rel{x}{y}{z}`.

This attempt is still brittle/broken in a few ways:
- It makes using braces in creative ways in mixfix notation ambiguous.
- It does not verify that the parameters are used in a consistent manner for each symbol. It essentially allows users to define  `a\MyRel b` and `a\MyRel{x} b` (and ones with even more parameters).
- It allows parameters for all relation symbols, even for those where it makes no sense in ordinary TeX markup, e.g. `a <{x} b`.
---
 library/topology/urysohntwo.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library')

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}.
-- 
cgit v1.2.3