Nuprl Lemma : metric-strong-extensionality
∀[X:Type]
∀d:metric(X)
(mcomplete(X with d)
⇒ (∀Y:Type. ∀d':metric(Y). ∀f:X ⟶ Y.
((∀x1,x2:X. (x1 ≡ x2 ⇒ f[x1] ≡ f[x2])) ⇒ (∀x1,x2:X. (f[x1] # f[x2] ⇒ x1 # x2)))))
Proof
Definitions occuring in Statement :
mcomplete: mcomplete(M),
mk-metric-space: X with d,
msep: x # y,
meq: x ≡ y,
metric: metric(X),
uall: ∀[x:A]. B[x],
so_apply: x[s],
all: ∀x:A. B[x],
implies: P ⇒ Q,
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
all: ∀x:A. B[x],
implies: P ⇒ Q,
so_apply: x[s],
prop: ℙ,
or: P ∨ Q,
not: ¬A,
false: False,
msep: x # y,
meq: x ≡ y,
mdist: mdist(d;x;y),
guard: {T},
uimplies: b supposing a,
uiff: uiff(P;Q),
and: P ∧ Q
Lemmas referenced :
metric-weak-Markov,
msep_wf,
meq_wf,
metric_wf,
mcomplete_wf,
mk-metric-space_wf,
istype-universe,
msep-or,
istype-void,
rless_transitivity1,
int-to-real_wf,
mdist_wf,
rleq_weakening,
rless_irreflexivity,
req_functionality,
mdist-symm,
req_weakening
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,
because_Cache,
universeIsType,
applyEquality,
inhabitedIsType,
sqequalRule,
functionIsType,
instantiate,
universeEquality,
unionElimination,
inlFormation_alt,
inrFormation_alt,
natural_numberEquality,
independent_isectElimination,
voidElimination,
productElimination
Latex:
\mforall{}[X:Type]
\mforall{}d:metric(X)
(mcomplete(X with d)
{}\mRightarrow{} (\mforall{}Y:Type. \mforall{}d':metric(Y). \mforall{}f:X {}\mrightarrow{} Y.
((\mforall{}x1,x2:X. (x1 \mequiv{} x2 {}\mRightarrow{} f[x1] \mequiv{} f[x2])) {}\mRightarrow{} (\mforall{}x1,x2:X. (f[x1] \# f[x2] {}\mRightarrow{} x1 \# x2)))))
Date html generated:
2019_10_30-AM-06_47_36
Last ObjectModification:
2019_10_02-AM-10_58_39
Theory : reals
Home
Index