AngouriMath

Navigation

← Back to list of members

Negation​(AngouriMath.​Entity,​AngouriMath.​Entity,​AngouriMath.​Entity.​Variable)

 Method (no overloads)

Summary

What not a is as a statement about x: the negation pushed
inward as far as there is an arm for it, and named as a set-builder where there is not.

Remarks

There was no arm for Notf at all, so every negation fell to
Empty — not (x = 1), not (x > 1) and
not (x in RR) each answered "no x satisfies this", which is a positive claim and
false of all three. That is the defect
#1036 fixed for
equations, left standing for negation.
#1127
Pushing the negation inward is unambiguous here in a way it is not in the
simplifier, which is why it is done here and not as a rule: this switch has arms for
the connectives and for the comparisons and none for not, so inward is the
direction that reaches one. A negated comparison is a comparison, and
InequalityEquality is where that is
already written down — asking it rather than restating it keeps the two from drifting.
What is left over is answered as written rather than as nothing: not (x in RR) is { x : not x in RR }, which names the non-real complex numbers exactly and
asserts of them only that they are what the statement says.

























Angouri © 2019-2023 · Project's repo · Site's repo · Octicons · Transparency · 4378 pages online