Nuprl Definition : compatible-rat-cubes
Compatible(c;d) == (↑Inhabited(c ⋂ d)) ⇒ (c ⋂ d ≤ c ∧ c ⋂ d ≤ d)
Definitions occuring in Statement :
inhabited-rat-cube: Inhabited(c),
rat-cube-intersection: c ⋂ d,
rat-cube-face: c ≤ d,
assert: ↑b,
implies: P ⇒ Q,
and: P ∧ Q
Definitions occuring in definition :
rat-cube-intersection: c ⋂ d,
rat-cube-face: c ≤ d,
and: P ∧ Q,
inhabited-rat-cube: Inhabited(c),
assert: ↑b,
implies: P ⇒ Q
FDL editor aliases :
compat-rc
compat-rc
Latex:
Compatible(c;d) == (\muparrow{}Inhabited(c \mcap{} d)) {}\mRightarrow{} (c \mcap{} d \mleq{} c \mwedge{} c \mcap{} d \mleq{} d)
Date html generated:
2019_10_29-AM-07_54_02
Last ObjectModification:
2019_10_17-PM-04_47_13
Theory : rationals
Home
Index