En matemáticas constructivas , una relación de desigualdad es una forma constructiva de desigualdad y a menudo se considera más básica que la igualdad .
Una relación de separación se escribe a menudo como (⧣ en Unicode ) para distinguirla de la negación de la igualdad (la negación de la desigualdad ), que es más débil. En la literatura, se encuentra que el símbolo se utiliza para cualquiera de estas dos.
Una relación binaria es una relación de separación si satisface: [1]
Por lo tanto, una relación de distanciamiento es una relación binaria irreflexiva simétrica con la condición adicional de que si dos elementos están separados, entonces cualquier otro elemento está separado de al menos uno de ellos. Esta última propiedad a menudo se denomina cotransitividad o comparación .
El complemento de una relación de separación es una relación de equivalencia , ya que las tres condiciones anteriores se convierten en reflexividad , simetría y transitividad . Si esta relación de equivalencia es de hecho igualdad, entonces la relación de separación se llama estrecha . Es decir, es unarelación de estrecha separación si además satisface:
En matemáticas clásicas , también se deduce que toda relación de separación es el complemento de una relación de equivalencia, y la única relación de separación estricta en un conjunto dado es el complemento de la igualdad. Por lo tanto, en ese ámbito, el concepto no es útil. En matemáticas constructivas, sin embargo, este no es el caso.
La relación de separación prototípica es la de los números reales: se dice que dos números reales están separados si existe (se puede construir) un número racional entre ellos. En otras palabras, los números reales y están separados si existe un número racional tal que o La relación de separación natural de los números reales es entonces la disyunción de su pseudoorden natural . Los números complejos , los espacios vectoriales reales y, de hecho, cualquier espacio métrico heredan naturalmente la relación de separación de los números reales, aunque no vengan equipados con ningún ordenamiento natural.
Si no hay ningún número racional entre dos números reales, entonces los dos números reales son iguales. Clásicamente, entonces, si dos números reales no son iguales, se concluiría que existe un número racional entre ellos. Sin embargo, de esto no se sigue que uno pueda realmente construir tal número. Por lo tanto, decir que dos números reales están separados es una afirmación más fuerte, constructivamente, que decir que no son iguales, y mientras que la igualdad de los números reales se puede definir en términos de su separación, la separación de los números reales no se puede definir en términos de su igualdad. Por esta razón, especialmente en topología constructiva, la relación de separación sobre un conjunto se toma a menudo como primitiva, y la igualdad es una relación definida.
Un conjunto dotado de una relación de separación se conoce como setoide constructivo . Una función entre estos setoides y puede llamarse morfismo para y si se cumple la propiedad de extensionalidad fuerte.
Esto debe compararse con la propiedad de extensionalidad de las funciones, es decir, que las funciones preservan la igualdad. De hecho, para la desigualdad de negación definida en la teoría de conjuntos común, la primera representa el contrapositivo de la segunda.
