Отношение обособленности

В конструктивной математике является отношение обособленности конструктивной формой неравенства и часто считается более фундаментальным, чем равенство .

Отношение обособленности часто записывается как $\#$ (⧣ в Юникоде ), чтобы отличить от отрицания равенства ( неравенства отрицания ), которое является более слабым. В литературе символ $\neq$ обнаруживается, что используется для любого из них.

Определение

Бинарное отношение $\#$ является отношением обособленности, если оно удовлетворяет:

1. $\neg (x\#x)$
2. $x\#y\;\to \;y\#x$
3. $x\#y\;\to \;(x\#z\;\vee \;y\#z)$

Таким образом, отношение отделенности — это симметричное иррефлексивное бинарное отношение с дополнительным условием: если два элемента разделены, то любой другой элемент отделен хотя бы от одного из них. Это последнее свойство часто называют котранзитивностью или сравнением .

Дополнением становятся отношения обособленности является отношение эквивалентности , поскольку вышеуказанные три условия рефлексивностью , симметрией и транзитивностью . Если это отношение эквивалентности на самом деле является равенством, то отношение обособленности называется тесным . То есть, $\#$ это строгое отношение обособленности, если оно дополнительно удовлетворяет:

4. $\neg (x\#y)\;\to \;x=y.$

Из классической математики также следует, что каждое отношение обособленности является дополнением отношения эквивалентности, а единственное строгое отношение обособленности в данном множестве является дополнением равенства. Так что в этой области эта концепция бесполезна. Однако в конструктивной математике это не так.

Примеры

Прототипическое отношение отделенности - это отношение действительных чисел: два действительных числа называются отдельными, если между ними существует (можно построить) рациональное число . Другими словами, действительные числа $x$ и $y$ разделены, если существует рациональное число $z$ такой, что $x<z<y$ или $y<z<x.$ Естественное отношение обособленности действительных чисел является тогда дизъюнкцией их естественного псевдопорядка . Комплексные числа , действительные векторные пространства и любое метрическое пространство естественным образом наследуют отношение отделенности действительных чисел, даже если они не оснащены каким-либо естественным упорядочением.

Если между двумя действительными числами нет рационального числа, то эти два действительных числа равны. Классически тогда, если два действительных числа не равны, можно было бы заключить, что между ними существует рациональное число. Однако из этого не следует, что такое число действительно можно построить. Таким образом, сказать, что два действительных числа разделены, с конструктивной точки зрения является более сильным утверждением, чем сказать, что они не равны, и хотя равенство действительных чисел можно определить с точки зрения их обособленности, раздельность действительных чисел не может быть определена с точки зрения их обособленности. равенство. По этой причине, особенно в конструктивной топологии , отношение отделенности над множеством часто считается примитивным, а равенство - определенным отношением.

Связанные определения

Множество, наделенное отношением обособленности, известно как конструктивный сетоид . Функция $f:A\to B$ между такими сетоидами $A$ и $B$ назвать морфизмом можно $\#_{A}$ и $\#_{B}$ если выполняется свойство сильной экстенсиональности

$\forall (x,\,y\colon A).\,f(x)\;\#_{B}\;f(y)\to x\;\#_{A}\;y.$

Это следует сравнить со свойством экстенсиональности функций, т. е. с тем, что функции сохраняют равенство.Действительно, для неравенства отрицания, определенного в общей теории множеств, первое представляет собой противоположность второму.

См. также

• Класс эквивалентности – математическое понятие