Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
added table of contents, section headers, and links to apartness relation, stable equality, Kock field
Anonymous
The half-sentence
It is taken for granted in classical mathematics.
needs a little addendum: What is it that is taken for granted?
Maybe it should rather say something like this:
In classical mathematics denial inequalities are just plain inequalities and so the notion plays no (further) role, classically.
replaced
It is taken for granted in classical mathematics.
with
In classical mathematics, denial inequalities and tight apartness relations are the same, so the notion plays no further role classically.
Anonymous
also changed
“other inequality relations such as apartness relations”
to
since those are the only ones which are different from denial inequalities in constructive mathematics. General apartness relations and other irreflexive symmetric relations are still relevant in other parts of mathematics, such as local rings, even in classical mathematics.
Anonymous
Thanks!
added properties of denial inequality under de Morgan’s law and under the double negation law.
Anonymous
1 to 6 of 6