Nuprl Lemma : decidable__squash_exists_fset
∀[T:Type]. ∀[P:T ⟶ ℙ]. ∀eq:EqDecider(T). ∀s:fset(T). ((∀x:T. Dec(P[x])) ⇒ Dec(↓∃x:T. (x ∈ s ∧ P[x])))
Proof
Definitions occuring in Statement :
fset-member: a ∈ s,
fset: fset(T),
deq: EqDecider(T),
decidable: Dec(P),
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[s],
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
squash: ↓T,
implies: P ⇒ Q,
and: P ∧ Q,
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
member: t ∈ T,
so_apply: x[s],
subtype_rel: A ⊆r B,
prop: ℙ,
decidable: Dec(P),
or: P ∨ Q,
iff: P ⇐⇒ Q,
and: P ∧ Q,
uimplies: b supposing a,
isl: isl(x),
not: ¬A,
false: False,
rev_implies: P ⇐ Q,
assert: ↑b,
ifthenelse: if b then t else f fi ,
btrue: tt,
true: True,
bfalse: ff,
so_lambda: λ2x.t[x],
guard: {T},
fset: fset(T),
exists: ∃x:A. B[x],
quotient: x,y:A//B[x; y],
squash: ↓T,
uiff: uiff(P;Q),
cand: A c∧ B,
fset-member: a ∈ s,
top: Top
Lemmas referenced :
decidable_wf,
isl_wf,
not_wf,
equal_wf,
assert_elim,
bfalse_wf,
btrue_neq_bfalse,
assert_wf,
assert_witness,
decidable__not,
fset-null_wf,
fset-filter_wf,
decidable__assert,
squash_wf,
exists_wf,
fset-member_wf,
all_wf,
fset_wf,
deq_wf,
equal-wf-base,
list_wf,
set-equal_wf,
decidable__l_exists,
assert-fset-null,
list_subtype_fset,
fset-filter-is-empty,
l_exists_iff,
l_member_wf,
assert-deq-member,
member-fset-filter,
mem_empty_lemma
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
lambdaFormation,
rename,
cut,
applyEquality,
functionExtensionality,
sqequalHypSubstitution,
hypothesisEquality,
cumulativity,
thin,
introduction,
extract_by_obid,
isectElimination,
hypothesis,
because_Cache,
sqequalRule,
equalityTransitivity,
equalitySymmetry,
dependent_functionElimination,
independent_functionElimination,
independent_pairFormation,
unionElimination,
addLevel,
voidEquality,
inrEquality,
independent_isectElimination,
levelHypothesis,
voidElimination,
natural_numberEquality,
lambdaEquality,
inlFormation,
productEquality,
inrFormation,
functionEquality,
universeEquality,
pointwiseFunctionalityForEquality,
pertypeElimination,
productElimination,
imageMemberEquality,
baseClosed,
setElimination,
setEquality,
dependent_pairFormation,
imageElimination,
hyp_replacement,
applyLambdaEquality,
isect_memberEquality
Latex:
\mforall{}[T:Type]. \mforall{}[P:T {}\mrightarrow{} \mBbbP{}].
\mforall{}eq:EqDecider(T). \mforall{}s:fset(T). ((\mforall{}x:T. Dec(P[x])) {}\mRightarrow{} Dec(\mdownarrow{}\mexists{}x:T. (x \mmember{} s \mwedge{} P[x])))
Date html generated:
2017_04_17-AM-09_20_08
Last ObjectModification:
2017_02_27-PM-05_23_43
Theory : finite!sets
Home
Index