Nuprl Definition : weak-connex
(basic):: weak-connex(T; x,y.R[x; y]) == ∀[x,y:T]. (↓R[x; y] ∨ R[y; x])
Definitions occuring in Statement :
uall: ∀[x:A]. B[x],
squash: ↓T,
or: P ∨ Q
Definitions occuring in definition :
uall: ∀[x:A]. B[x],
squash: ↓T,
or: P ∨ Q
Latex:
(basic):: weak-connex(T; x,y.R[x; y]) == \mforall{}[x,y:T]. (\mdownarrow{}R[x; y] \mvee{} R[y; x])
Date html generated:
2016_05_13-PM-04_16_09
Last ObjectModification:
2015_09_22-PM-05_46_08
Theory : rel_1
Home
Index