Proximity Structure

In General > s.a. uniformity.
* Idea: A proximity space is an intermediate concept between those of a topological space and a uniform space.
$Def: An (Efremovich) proximity on a set X is a binary relation δ on the power set of X which obeys: (1) If (A δ B) then (B δ A) (symmetry); (2) (AB) δ C iff (A δ C) $$\lor$$ (B δ C); (3) If (A δ B) then A, B ≠ Ø; (4) If ¬ (A δ B) then there exists E such that ¬ (A δ E) ∧ ¬ (X \ E) δ B; (5) If AB ≠ Ø then (A δ B). * Relationships: It induces a topology by A':= {x | x δ A}, for all AX; This topology is always completely regular (and viceversa), and Tychonov if δ is separated. Special Types and Examples * Special case: If (6) (x δ y) implies (x = y), then the proximity is called separated (Hausdorff). * Examples: The discrete proximity, defined by A δ B iff AB ≠ Ø; The indiscrete proximity, in which A δ B iff A, B ≠ Ø. References @ General: Naimpally & Warrack 70; Bridges & Vîţă 11 [using constructive logic]. > Online resources: see nLab page. Proximity Map$ Def: Given a set X and a group G, a map δ: X × XG such that for all xX, δ(x, x) = 1.