Nuprl Definition : rat-sub-interval
rat-sub-interval(I;J) == let a,b = I in let c,d = J in ((c ≤ a) ∧ (b ≤ d)) ∧ (c < d ⇒ a < b)
Definitions occuring in Statement :
qle: r ≤ s,
qless: r < s,
implies: P ⇒ Q,
and: P ∧ Q,
spread: spread def
Definitions occuring in definition :
spread: spread def,
and: P ∧ Q,
qle: r ≤ s,
implies: P ⇒ Q,
qless: r < s
FDL editor aliases :
rat-sub-interval
Latex:
rat-sub-interval(I;J) == let a,b = I in let c,d = J in ((c \mleq{} a) \mwedge{} (b \mleq{} d)) \mwedge{} (c < d {}\mRightarrow{} a < b)
Date html generated:
2020_05_20-AM-09_17_21
Last ObjectModification:
2019_11_14-PM-10_55_14
Theory : rationals
Home
Index