Nuprl Definition : same_order
same_order(x1;y1;x2;y2;L;T) == x1 << y1 ∈ L ⇒ (x2 ∈ L) ⇒ (y2 ∈ L) ⇒ x2 << y2 ∈ L
Definitions occuring in Statement :
strong_before: x << y ∈ l,
l_member: (x ∈ l),
implies: P ⇒ Q
Definitions occuring in definition :
implies: P ⇒ Q,
l_member: (x ∈ l),
strong_before: x << y ∈ l
FDL editor aliases :
same_order
Latex:
same\_order(x1;y1;x2;y2;L;T) == x1 << y1 \mmember{} L {}\mRightarrow{} (x2 \mmember{} L) {}\mRightarrow{} (y2 \mmember{} L) {}\mRightarrow{} x2 << y2 \mmember{} L
Date html generated:
2016_05_15-PM-01_53_43
Last ObjectModification:
2015_09_23-AM-07_37_23
Theory : list!
Home
Index