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

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

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

Бинарное отношение является отношением обособленности, если оно удовлетворяет: ^[1]${\displaystyle \#}$

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

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

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

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

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

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

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

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

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

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

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