Re: [tlaplus] << >> = { }

[fl <freder...@xxxxxxxxxxx>]

 

Excuse me. No what is defined by IsAFcn is the operator [ x \in A |-> B ] not

IsAFcn. I had missed the equality.

 

 

 

For those who are interested, the property used by TLA+ to define a function would be in

a traditional presentation of ZFC:

 

http://us2.metamath.org:88/mpegif/dffn5.html

 

But even in that case it would be a relation.

 

--

FL