Nuprl Lemma : lsum_cons_lemma
∀as,a,f:Top. (Σ(f[x] | x ∈ [a / as]) ~ f[a] + Σ(f[x] | x ∈ as))
Proof
Definitions occuring in Statement :
lsum: Σ(f[x] | x ∈ L),
cons: [a / b],
top: Top,
so_apply: x[s],
all: ∀x:A. B[x],
add: n + m,
sqequal: s ~ t
Definitions unfolded in proof :
lsum: Σ(f[x] | x ∈ L),
all: ∀x:A. B[x],
member: t ∈ T,
top: Top
Lemmas referenced :
map_cons_lemma,
istype-void,
l_sum_cons_lemma,
istype-top
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
isect_memberEquality_alt,
voidElimination,
hypothesis,
lambdaFormation_alt,
inhabitedIsType,
hypothesisEquality
Latex:
\mforall{}as,a,f:Top. (\mSigma{}(f[x] | x \mmember{} [a / as]) \msim{} f[a] + \mSigma{}(f[x] | x \mmember{} as))
Date html generated:
2020_05_19-PM-09_46_55
Last ObjectModification:
2019_11_12-PM-11_23_53
Theory : list_1
Home
Index