Skip to content

Commit

Permalink
remove suspicious definition; restore 'klr 5'
Browse files Browse the repository at this point in the history
  • Loading branch information
benjub committed Aug 15, 2023
1 parent 06cca95 commit 7e300b7
Showing 1 changed file with 1 addition and 17 deletions.
18 changes: 1 addition & 17 deletions set.mm
Original file line number Diff line number Diff line change
Expand Up @@ -360,7 +360,7 @@ useful for discussing objects (beyond simply true or false). In particular,
$( $j
syntax 'wff';
syntax '|-' as 'wff';
unambiguous 'klr 12';
unambiguous 'klr 5';
$)

$( Declare typographical constant symbols that are not directly used
Expand Down Expand Up @@ -529148,22 +529148,6 @@ automatically a set (see ~ bj-mooreset ). (Contributed by BJ,
PUSURFGUOHUBUETUFTUGUHCIUMFUIABIDEGCUJUK $.
$}

$( Syntax for maps-to notation for functions with two arguments. $)
cmpt2-bj $a class ( <. x , y >. e. A |-> B ) $.

${
$d z x $. $d z y $. $d z A $. $d z B $.
$( Define maps-to notation for functions with two arguments. When ` A ` is
replaced by a product ` ( C X. D ) ` , this is equivalent to ~ df-mpo ,
but it is more compact, and is read more easily as a function of two
arguments (which can be hard with ~ df-mpo when the above ` C ` is
replaced with a long expression). This definition is also more
versatile, since it can describe for instance a function on the unit
disc in ` RR^ 2 ` . (Contributed by BJ, 15-Aug-2023.) $)
df-bj-mpt2 $a |- ( <. x , y >. e. A |-> B ) =
{ <. <. x , y >. , z >. | ( <. x , y >. e. A /\ z = B ) } $.
$}

$( Syntax for maps-to notation for functions with three arguments. $)
cmpt3 $a class ( x e. A , y e. B , z e. C |-> D ) $.

Expand Down

0 comments on commit 7e300b7

Please sign in to comment.