Nuprl Lemma : m-strong-extensionality
∀[X:Type]. ∀d:metric(X). (mcomplete(X with d) ⇒ (∀Y:Type. ∀d':metric(Y). ∀f:FUN(X ⟶ Y). is-msfun(X;d;Y;d';f)))
Proof
Definitions occuring in Statement :
mcomplete: mcomplete(M),
is-msfun: is-msfun(X;d;Y;d';f),
mfun: FUN(X ⟶ Y),
mk-metric-space: X with d,
metric: metric(X),
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
all: ∀x:A. B[x],
implies: P ⇒ Q,
mfun: FUN(X ⟶ Y),
sq_stable: SqStable(P),
prop: ℙ,
is-msfun: is-msfun(X;d;Y;d';f),
squash: ↓T,
guard: {T},
is-mfun: f:FUN(X;Y)
Lemmas referenced :
metric-strong-extensionality,
sq_stable__is-msfun,
meq_wf,
mfun_wf,
metric_wf,
mcomplete_wf,
mk-metric-space_wf,
istype-universe
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
hypothesis,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
lambdaFormation_alt,
dependent_functionElimination,
independent_functionElimination,
setElimination,
rename,
because_Cache,
universeIsType,
inhabitedIsType,
sqequalRule,
imageMemberEquality,
baseClosed,
imageElimination,
instantiate,
universeEquality
Latex:
\mforall{}[X:Type]
\mforall{}d:metric(X)
(mcomplete(X with d) {}\mRightarrow{} (\mforall{}Y:Type. \mforall{}d':metric(Y). \mforall{}f:FUN(X {}\mrightarrow{} Y). is-msfun(X;d;Y;d';f)))
Date html generated:
2019_10_30-AM-06_47_56
Last ObjectModification:
2019_10_02-AM-10_58_57
Theory : reals
Home
Index