Nuprl Lemma : finite-type-product
∀[A:Type]. ∀[B:A ⟶ Type]. (finite-type(A) ⇒ (∀a:A. finite-type(B[a])) ⇒ finite-type(a:A × B[a]))
Proof
Definitions occuring in Statement :
finite-type: finite-type(T),
uall: ∀[x:A]. B[x],
so_apply: x[s],
all: ∀x:A. B[x],
implies: P ⇒ Q,
function: x:A ⟶ B[x],
product: x:A × B[x],
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
all: ∀x:A. B[x],
member: t ∈ T,
so_apply: x[s],
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q,
exists: ∃x:A. B[x],
pi1: fst(t),
prop: ℙ,
cand: A c∧ B,
guard: {T}
Lemmas referenced :
finite-type-iff-list,
finite-type_wf,
istype-universe,
concat_wf,
map_wf,
list_wf,
l_member_wf,
member-concat,
member_map
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
lambdaFormation_alt,
cut,
hypothesis,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesisEquality,
introduction,
extract_by_obid,
isectElimination,
applyEquality,
productElimination,
independent_functionElimination,
because_Cache,
productEquality,
sqequalRule,
functionIsType,
universeIsType,
inhabitedIsType,
instantiate,
universeEquality,
rename,
dependent_pairFormation_alt,
lambdaEquality_alt,
dependent_pairEquality_alt,
equalityIstype,
equalityTransitivity,
equalitySymmetry,
productIsType,
independent_pairFormation
Latex:
\mforall{}[A:Type]. \mforall{}[B:A {}\mrightarrow{} Type]. (finite-type(A) {}\mRightarrow{} (\mforall{}a:A. finite-type(B[a])) {}\mRightarrow{} finite-type(a:A \mtimes{} B[a]))
Date html generated:
2019_10_15-AM-11_13_14
Last ObjectModification:
2018_11_30-AM-10_15_12
Theory : general
Home
Index