Nuprl Definition : sum_of_torder
sum_of_torder(T;R) == ∀a,b,x:T. ((((R a x) ∧ (R b x)) ∨ ((R x a) ∧ (R x b))) ⇒ (((R a b) ∨ (a = b ∈ T)) ∨ (R b a)))
Definitions occuring in Statement :
all: ∀x:A. B[x],
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
apply: f a,
equal: s = t ∈ T
Definitions occuring in definition :
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
or: P ∨ Q,
equal: s = t ∈ T,
apply: f a
FDL editor aliases :
sum_of_torder
Latex:
sum\_of\_torder(T;R) ==
\mforall{}a,b,x:T. ((((R a x) \mwedge{} (R b x)) \mvee{} ((R x a) \mwedge{} (R x b))) {}\mRightarrow{} (((R a b) \mvee{} (a = b)) \mvee{} (R b a)))
Date html generated:
2016_05_15-PM-04_54_36
Last ObjectModification:
2015_09_23-AM-07_50_53
Theory : general
Home
Index