Nuprl Lemma : per-apply_wf
∀[A:Type]. ∀[B:type-function{i:l}(A)]. ∀[f:per-function(A;a.B[a])]. ∀[a:A]. (per-apply(f;a) ∈ tf-apply(B;a))
Proof
Definitions occuring in Statement :
per-apply: per-apply(f;x),
tf-apply: tf-apply(f;x),
type-function: type-function{i:l}(A),
per-function: per-function(A;a.B[a]),
uall: ∀[x:A]. B[x],
so_apply: x[s],
member: t ∈ T,
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
so_apply: x[s],
per-apply: per-apply(f;x),
tf-apply: tf-apply(f;x)
Lemmas referenced :
per-function_wf,
type-function_wf,
apply-wf-per
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
cut,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
introduction,
hypothesis,
sqequalRule,
axiomEquality,
equalityTransitivity,
equalitySymmetry,
because_Cache,
universeEquality
Latex:
\mforall{}[A:Type]. \mforall{}[B:type-function\{i:l\}(A)]. \mforall{}[f:per-function(A;a.B[a])]. \mforall{}[a:A].
(per-apply(f;a) \mmember{} tf-apply(B;a))
Date html generated:
2016_05_13-PM-03_54_00
Last ObjectModification:
2015_12_26-AM-10_40_50
Theory : per!type
Home
Index