Nuprl Lemma : per-function-ext
∀[A:Type]. ∀[B:per-function(A;x.Type)]. ∀[f,g:per-function(A;x.B[x])].
f = g ∈ per-function(A;x.B[x]) supposing ∀[a:A]. ((f a) = (g a) ∈ B[a])
Proof
Definitions occuring in Statement :
per-function: per-function(A;a.B[a]),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
so_apply: x[s],
apply: f a,
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
type-function: type-function{i:l}(A),
so_apply: x[s],
uimplies: b supposing a,
guard: {T},
all: ∀x:A. B[x],
implies: P ⇒ Q,
prop: ℙ,
pi2: snd(t),
pi1: fst(t),
top: Top,
so_lambda: λ2x.t[x],
subtype_rel: A ⊆r B,
cand: A c∧ B,
and: P ∧ Q,
sq_type: SQType(T),
per-function: per-function(A;a.B[a]),
function-eq: function-eq(A;a.B[a];f;g),
per-apply: per-apply(f;x),
tf-apply: tf-apply(f;x),
true: True,
label: ...$L... t,
squash: ↓T,
rev_implies: P ⇐ Q,
iff: P ⇐⇒ Q
Lemmas referenced :
per-function_wf_type,
per-function-type-apply,
per-function_wf,
apply-wf-per,
istype-universe,
equal_wf,
base_wf,
top_wf,
subtype_rel_product,
pair-eta,
pi1_wf,
pi2_wf,
subtype_rel_self,
product_subtype_base,
subtype_base_sq,
uall_wf,
equal-wf-base,
type-function_wf,
true_wf,
squash_wf,
per-apply_wf,
type-function-eta,
tf-apply_wf,
istype-top,
istype-void,
member_wf,
equal-wf-T-base
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :isect_memberFormation_alt,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
because_Cache,
sqequalRule,
Error :isectIsType,
Error :universeIsType,
Error :equalityIsType1,
hypothesis,
instantiate,
universeEquality,
independent_pairEquality,
Error :inhabitedIsType,
Error :lambdaFormation_alt,
pointwiseFunctionality,
equalityTransitivity,
equalitySymmetry,
dependent_functionElimination,
independent_functionElimination,
productElimination,
productEquality,
baseClosed,
closedConclusion,
baseApply,
lambdaFormation,
voidEquality,
voidElimination,
isect_memberEquality,
independent_isectElimination,
lambdaEquality,
applyEquality,
independent_pairFormation,
applyLambdaEquality,
cumulativity,
axiomEquality,
pertypeMemberEquality,
imageMemberEquality,
natural_numberEquality,
imageElimination,
hyp_replacement,
Error :lambdaEquality_alt,
Error :isect_memberEquality_alt,
functionEquality,
Error :dependent_set_memberEquality_alt,
Error :productIsType,
Error :equalityIsType3,
setElimination,
rename,
isectEquality,
promote_hyp
Latex:
\mforall{}[A:Type]. \mforall{}[B:per-function(A;x.Type)]. \mforall{}[f,g:per-function(A;x.B[x])].
f = g supposing \mforall{}[a:A]. ((f a) = (g a))
Date html generated:
2019_06_20-AM-11_30_08
Last ObjectModification:
2018_11_20-PM-03_20_21
Theory : per!type
Home
Index