[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

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:
But even in that case it would be a relation.