차별성 관계

건설적인 수학에서, 분리관계는 불평등의 건설적인 형태로서, 종종 평등보다 더 기본적인 것으로 받아들여진다.흔히 더 약한 평등의 부정(부정 불평등) ≠과 구별하기 위해 #로 쓰여진다.

설명

차별성 관계는 두 요소가 떨어져 있으면 다른 어떤 요소도 적어도 한 요소로부터 떨어져 있다는 추가 조건과 대칭적으로 회복할 수 없는 이항 관계다(이 마지막 속성을 종종 공동 변환 또는 비교라고 한다).

즉,^[1] 2진수 관계 #는 다음과 같은 경우 분리성 관계다.

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

위의 세 가지 조건이 반사성, 대칭성, 전이성이 되므로, 차별성 관계의 보완은 동등성 관계다.만약 이 동등성 관계가 사실상 동등하다면, 그 차별성 관계를 타이트하다고 부른다.즉, #는 추가로 다음을 만족하는 경우 엄격한 차별성 관계가 된다.

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

고전 수학에서 또한 모든 차별성 관계는 동등성 관계의 보완이며, 주어진 집합에서 유일한 엄격한 차별성 관계는 평등의 보완이라는 것을 따른다.그래서 그 영역에서는 그 개념이 유용하지 않다.그러나 건설 수학에서는 그렇지 않다.

표준적인 차별성 관계는 실수의 관계인데, 두 개의 실수는 그들 사이에 이성적인 숫자가 존재한다면(하나의 실수는 구성될 수 있다) 떨어져 있다고 한다.즉, x < z < y> 또는 y < x < x>와 같은 합리적인 숫자 z가 존재한다면 실수는 x와 y가 분리된다.실제 숫자의 자연적인 별따기 관계는 그 자연적인 사이비 질서의 분리가 된다.복잡한 숫자, 실제 벡터 공간, 그리고 실제로 어떤 메트릭스 공간은 자연적인 순서가 갖추어지지 않았음에도 불구하고 자연적으로 실제 숫자의 차별성 관계를 이어받는다.

만약 두 실수 사이에 합리적인 숫자가 없다면, 두 실수는 같다.고전적으로, 그렇다면, 만약 두 개의 실제 숫자가 같지 않다면, 그 사이에 합리적인 숫자가 존재한다고 결론을 내릴 것이다.그러나 실제로 그런 숫자를 만들 수 있는 것은 아니다.따라서 두 개의 실제 숫자가 분리되어 있다고 말하는 것은 그들이 같지 않다고 말하는 것보다 건설적으로 더 강력한 진술이며, 실제 숫자의 동일성은 그들의 분리성 측면에서 정의될 수 있지만, 실제 숫자의 차별성은 그들의 평등성 측면에서 정의될 수 없다.이러한 이유로, 특히 건설적인 토폴로지에서는 집합에 대한 차별성 관계를 원시적인 것으로 받아들이는 경우가 많으며, 평등은 정의된 관계다.

차별성 관계가 부여된 세트를 건설적인 세토이드라고 한다.함수 $f{\displaystyle }$: ${\displaystyle A}$→ B ${\displaystyle f:$$A\rightarrow B}$ where A and B are constructive setoids is called a morphism for #_A and #_B if ${\displaystyle \forall x,\,y:A.\,f(x)\;\#_{B}\;f(y)\Rightarrow x\;\#_{$$A}\;y$

참조