Nuprl Definition : R-closed

R-closed(T;x.X[x];a,b.R[a; b]) ==  ∀a,b:T.  (R[a; b] ⇒ X[a] ⇒ X[b])


Definitions occuring in Statement :  all: ∀x:A. B[x],  implies: P ⇒ Q
Definitions occuring in definition :  all: ∀x:A. B[x],  implies: P ⇒ Q
FDL editor aliases :  R-closed
Latex:
R-closed(T;x.X[x];a,b.R[a;  b])  ==    \mforall{}a,b:T.    (R[a;  b]  {}\mRightarrow{}  X[a]  {}\mRightarrow{}  X[b])


Date html generated: 2016_05_14-PM-04_08_50
Last ObjectModification: 2015_09_22-PM-06_02_12

Theory : fan-theorem


Home Index