Nuprl Lemma : ball_respects_bsublist
∀s:DSet. ∀us,vs:|s| List.
((↑bsublist(s;us;vs)) ⇒ (∀Q:|s| ⟶ 𝔹. ((↑(For{<𝔹,∧b>} x ∈ vs. Q[x])) ⇒ (↑(For{<𝔹,∧b>} x ∈ us. Q[x])))))
Proof
Definitions occuring in Statement :
bsublist: bsublist(s;as;bs),
mon_for: For{g} x ∈ as. f[x],
list: T List,
assert: ↑b,
bool: 𝔹,
so_apply: x[s],
all: ∀x:A. B[x],
implies: P ⇒ Q,
function: x:A ⟶ B[x],
band_mon: <𝔹,∧b>,
dset: DSet,
set_car: |p|
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
member: t ∈ T,
prop: ℙ,
uall: ∀[x:A]. B[x],
subtype_rel: A ⊆r B,
guard: {T},
uimplies: b supposing a,
dset: DSet,
so_lambda: λ2x.t[x],
so_apply: x[s],
band_mon: <𝔹,∧b>,
grp_car: |g|,
pi1: fst(t),
abmonoid: AbMon,
mon: Mon,
exists: ∃x:A. B[x],
uiff: uiff(P;Q),
and: P ∧ Q,
infix_ap: x f y,
grp_op: *,
pi2: snd(t)
Lemmas referenced :
assert_wf,
mon_for_wf,
band_mon_wf,
iabmonoid_subtype_imon,
abmonoid_subtype_iabmonoid,
subtype_rel_transitivity,
abmonoid_wf,
iabmonoid_wf,
imon_wf,
set_car_wf,
bool_wf,
grp_car_wf,
bsublist_wf,
list_wf,
dset_wf,
bsublist_append_diff,
append_wf,
mem_f_wf,
assert_functionality_wrt_uiff,
mon_for_functionality_wrt_permr,
permr_inversion,
grp_op_wf,
mon_for_append,
assert_of_band
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
dependent_functionElimination,
hypothesis,
applyEquality,
instantiate,
independent_isectElimination,
sqequalRule,
setElimination,
rename,
hypothesisEquality,
lambdaEquality,
functionEquality,
independent_functionElimination,
productElimination,
because_Cache
Latex:
\mforall{}s:DSet. \mforall{}us,vs:|s| List.
((\muparrow{}bsublist(s;us;vs))
{}\mRightarrow{} (\mforall{}Q:|s| {}\mrightarrow{} \mBbbB{}. ((\muparrow{}(For\{<\mBbbB{},\mwedge{}\msubb{}>\} x \mmember{} vs. Q[x])) {}\mRightarrow{} (\muparrow{}(For\{<\mBbbB{},\mwedge{}\msubb{}>\} x \mmember{} us. Q[x])))))
Date html generated:
2016_05_16-AM-07_41_58
Last ObjectModification:
2015_12_28-PM-05_41_46
Theory : list_2
Home
Index