Nuprl Lemma : dep-isect-value-type
∀A:Type. ∀B:A ⟶ Type. ((value-type(A) ∨ (∀a:A. value-type(B[a]))) ⇒ value-type(a:A ⋂ B[a]))
Proof
Definitions occuring in Statement :
dep-isect: x:A ⋂ B[x],
value-type: value-type(T),
so_apply: x[s],
all: ∀x:A. B[x],
implies: P ⇒ Q,
or: P ∨ Q,
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
value-type: value-type(T),
uall: ∀[x:A]. B[x],
uimplies: b supposing a,
member: t ∈ T,
sq_stable: SqStable(P),
so_lambda: λ2x.t[x],
so_apply: x[s],
has-value: (a)↓,
prop: ℙ,
squash: ↓T,
or: P ∨ Q,
guard: {T}
Lemmas referenced :
sq_stable__has-value,
dep-isect_wf,
equal_wf,
equal-wf-base,
base_wf,
or_wf,
value-type_wf,
all_wf,
value-type-has-value
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
isect_memberFormation,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
independent_functionElimination,
equalityTransitivity,
equalitySymmetry,
dependent_functionElimination,
cumulativity,
sqequalRule,
lambdaEquality,
applyEquality,
functionExtensionality,
instantiate,
imageMemberEquality,
baseClosed,
imageElimination,
because_Cache,
functionEquality,
universeEquality,
dependentIntersectionElimination,
unionElimination,
independent_isectElimination
Latex:
\mforall{}A:Type. \mforall{}B:A {}\mrightarrow{} Type. ((value-type(A) \mvee{} (\mforall{}a:A. value-type(B[a]))) {}\mRightarrow{} value-type(a:A \mcap{} B[a]))
Date html generated:
2018_07_25-PM-01_30_24
Last ObjectModification:
2018_06_09-PM-09_18_15
Theory : dependent!intersection
Home
Index