Nuprl Lemma : member-f-union-aux
∀[T,A:Type].
∀eqt:EqDecider(T). ∀eqa:EqDecider(A). ∀g:T ⟶ fset(A). ∀L:T List. ∀a:A.
(a ∈ f-union(eqt;eqa;L;x.g[x]) ⇐⇒ (∃x∈L. a ∈ g[x]))
Proof
Definitions occuring in Statement :
f-union: f-union(domeq;rngeq;s;x.g[x]),
fset-member: a ∈ s,
fset: fset(T),
l_exists: (∃x∈L. P[x]),
list: T List,
deq: EqDecider(T),
uall: ∀[x:A]. B[x],
so_apply: x[s],
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
f-union: f-union(domeq;rngeq;s;x.g[x]),
member: t ∈ T,
so_lambda: λ2x.t[x],
so_lambda: λ2x y.t[x; y],
so_apply: x[s],
so_apply: x[s1;s2],
prop: ℙ,
implies: P ⇒ Q,
top: Top,
iff: P ⇐⇒ Q,
and: P ∧ Q,
guard: {T},
or: P ∨ Q,
subtype_rel: A ⊆r B,
rev_implies: P ⇐ Q,
false: False,
not: ¬A,
fset-member: a ∈ s,
assert: ↑b,
ifthenelse: if b then t else f fi ,
deq-member: x ∈b L,
reduce: reduce(f;k;as),
list_ind: list_ind,
nil: [],
it: ⋅,
bfalse: ff,
fset: fset(T),
uimplies: b supposing a
Lemmas referenced :
list_wf,
fset_wf,
deq_wf,
list_induction,
all_wf,
iff_wf,
fset-member_wf,
list_accum_wf,
fset-union_wf,
or_wf,
l_exists_wf,
l_member_wf,
list_accum_nil_lemma,
list_accum_cons_lemma,
l_exists_wf_nil,
fset-member_witness,
l_exists_nil,
l_exists_cons,
cons_wf,
member-fset-union,
set-equal_wf,
set-equal-equiv,
nil_wf,
set-equal-reflex,
quotient-member-eq
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
lambdaFormation,
hypothesisEquality,
cut,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesis,
functionEquality,
universeEquality,
sqequalRule,
lambdaEquality,
cumulativity,
because_Cache,
applyEquality,
setElimination,
rename,
setEquality,
independent_functionElimination,
dependent_functionElimination,
isect_memberEquality,
voidElimination,
voidEquality,
independent_pairFormation,
inrFormation,
introduction,
unionElimination,
productElimination,
addLevel,
allFunctionality,
impliesFunctionality,
orFunctionality,
inlFormation,
independent_isectElimination,
equalityTransitivity,
equalitySymmetry
Latex:
\mforall{}[T,A:Type].
\mforall{}eqt:EqDecider(T). \mforall{}eqa:EqDecider(A). \mforall{}g:T {}\mrightarrow{} fset(A). \mforall{}L:T List. \mforall{}a:A.
(a \mmember{} f-union(eqt;eqa;L;x.g[x]) \mLeftarrow{}{}\mRightarrow{} (\mexists{}x\mmember{}L. a \mmember{} g[x]))
Date html generated:
2016_05_14-PM-03_39_10
Last ObjectModification:
2015_12_26-PM-06_42_23
Theory : finite!sets
Home
Index