Nuprl Definition : anti_sym
(basic):: AntiSym(T;x,y.R[x; y]) == ∀x,y:T. (R[x; y] ⇒ R[y; x] ⇒ (x = y ∈ T))
Definitions occuring in Statement :
all: ∀x:A. B[x],
implies: P ⇒ Q,
equal: s = t ∈ T
Definitions occuring in definition :
all: ∀x:A. B[x],
implies: P ⇒ Q,
equal: s = t ∈ T
FDL editor aliases :
anti_sym
Latex:
(basic):: AntiSym(T;x,y.R[x; y]) == \mforall{}x,y:T. (R[x; y] {}\mRightarrow{} R[y; x] {}\mRightarrow{} (x = y))
Date html generated:
2016_05_13-PM-04_15_46
Last ObjectModification:
2015_09_22-PM-05_46_05
Theory : rel_1
Home
Index