Nuprl Lemma : inhabited-intersection-half-cubes
∀k:ℕ. ∀a,b,c,d:ℚCube(k).
((↑is-half-cube(k;c;a)) ⇒ (↑is-half-cube(k;d;b)) ⇒ (↑Inhabited(c ⋂ d)) ⇒ (↑Inhabited(a ⋂ b)))
Proof
Definitions occuring in Statement :
inhabited-rat-cube: Inhabited(c),
rat-cube-intersection: c ⋂ d,
is-half-cube: is-half-cube(k;h;c),
rational-cube: ℚCube(k),
nat: ℕ,
assert: ↑b,
all: ∀x:A. B[x],
implies: P ⇒ Q
Definitions unfolded in proof :
squash: ↓T,
qge: a ≥ b,
true: True,
lt_int: i <z j,
qmul: r * s,
qadd: r + s,
qsub: r - s,
qpositive: qpositive(r),
bor: p ∨bq,
q_le: q_le(r;s),
qadd_grp: <ℚ+>,
pi2: snd(t),
pi1: fst(t),
grp_le: ≤b,
infix_ap: x f y,
grp_leq: a ≤ b,
qle: r ≤ s,
false: False,
assert: ↑b,
eq_int: (i =z j),
btrue: tt,
evalall: evalall(t),
callbyvalueall: callbyvalueall,
qeq: qeq(r;s),
not: ¬A,
subtype_rel: A ⊆r B,
qavg: qavg(a;b),
ifthenelse: if b then t else f fi ,
band: p ∧b q,
bfalse: ff,
sq_type: SQType(T),
rev_implies: P ⇐ Q,
or: P ∨ Q,
guard: {T},
is-half-interval: is-half-interval(I;J),
inhabited-rat-interval: Inhabited(I),
rat-interval-intersection: I ⋂ J,
rational-interval: ℚInterval,
cand: A c∧ B,
rev_uimplies: rev_uimplies(P;Q),
iff: P ⇐⇒ Q,
prop: ℙ,
rational-cube: ℚCube(k),
nat: ℕ,
rat-cube-intersection: c ⋂ d,
uimplies: b supposing a,
and: P ∧ Q,
uiff: uiff(P;Q),
member: t ∈ T,
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
all: ∀x:A. B[x]
Lemmas referenced :
qadd_inv_assoc_q,
mon_ident_q,
qinverse_q,
qadd_ac_1_q,
qadd_comm_q,
qadd_preserves_qle,
subtype_rel_self,
qmul-qdiv-cancel,
true_wf,
squash_wf,
qle_weakening_eq_qorder,
qle_functionality_wrt_implies,
int-subtype-rationals,
qmul_wf,
qle_witness,
qadd_wf,
qdiv_wf,
qmul_preserves_qle2,
qavg-qle-iff-1,
qle-qavg-iff-1,
assert_of_band,
assert_of_bor,
iff_transitivity,
iff_weakening_equal,
assert-q_le-eq,
q_le_wf,
rationals_wf,
equal_wf,
bfalse_wf,
assert-qeq,
btrue_wf,
band_wf,
eqtt_to_assert,
bool_subtype_base,
bool_wf,
subtype_base_sq,
bool_cases,
qeq_wf2,
bor_wf,
qmax_lb,
qmax_wf,
qmin_ub,
qmin_wf,
qle_wf,
qavg_wf,
istype-nat,
rational-cube_wf,
assert-is-half-cube,
is-half-cube_wf,
assert_wf,
iff_weakening_uiff,
is-half-interval_wf,
int_seg_wf,
inhabited-rat-cube_wf,
istype-assert,
rat-cube-intersection_wf,
assert-inhabited-rat-cube
Rules used in proof :
minusEquality,
universeEquality,
imageMemberEquality,
imageElimination,
lambdaEquality_alt,
isect_memberFormation_alt,
sqequalBase,
baseClosed,
voidElimination,
applyLambdaEquality,
hyp_replacement,
inrFormation_alt,
inlFormation_alt,
isect_memberEquality_alt,
unionEquality,
cumulativity,
instantiate,
unionElimination,
promote_hyp,
productEquality,
unionIsType,
productIsType,
equalitySymmetry,
equalityTransitivity,
equalityIstype,
inhabitedIsType,
independent_pairFormation,
dependent_functionElimination,
functionEquality,
independent_functionElimination,
applyEquality,
rename,
setElimination,
natural_numberEquality,
universeIsType,
functionIsType,
sqequalRule,
independent_isectElimination,
productElimination,
hypothesis,
hypothesisEquality,
because_Cache,
thin,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
cut,
lambdaFormation_alt,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}k:\mBbbN{}. \mforall{}a,b,c,d:\mBbbQ{}Cube(k).
((\muparrow{}is-half-cube(k;c;a)) {}\mRightarrow{} (\muparrow{}is-half-cube(k;d;b)) {}\mRightarrow{} (\muparrow{}Inhabited(c \mcap{} d)) {}\mRightarrow{} (\muparrow{}Inhabited(a \mcap{} b)))
Date html generated:
2019_10_29-AM-07_54_51
Last ObjectModification:
2019_10_22-PM-04_05_02
Theory : rationals
Home
Index