Nuprl Lemma : simple-glueing
∀[X:Type]. ∀[dX:metric(X)]. ∀[A,B:X ⟶ ℙ].
((∀x1,x2:X. (x1 ≡ x2 ⇒ A[x1] ⇒ A[x2]))
⇒ (∀x1,x2:X. (x1 ≡ x2 ⇒ B[x1] ⇒ B[x2]))
⇒ (∀x:X. (A[x] ∨ B[x]))
⇒ (∀[Y:Type]. ∀[dY:metric(Y)].
∀f:FUN({x:X| A[x]} ⟶ Y). ∀g:FUN({x:X| B[x]} ⟶ Y).
∃h:FUN(X ⟶ Y). ∀x:X. ((A[x] ⇒ h x ≡ f x) ∧ (B[x] ⇒ h x ≡ g x))
supposing ∀x:X. ((A[x] ∧ B[x]) ⇒ f x ≡ g x)))
Proof
Definitions occuring in Statement :
mfun: FUN(X ⟶ Y),
meq: x ≡ y,
metric: metric(X),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[s],
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
all: ∀x:A. B[x],
uimplies: b supposing a,
member: t ∈ T,
meq: x ≡ y,
metric: metric(X),
mfun: FUN(X ⟶ Y),
and: P ∧ Q,
so_apply: x[s],
subtype_rel: A ⊆r B,
prop: ℙ,
exists: ∃x:A. B[x],
or: P ∨ Q,
is-mfun: f:FUN(X;Y),
guard: {T},
cand: A c∧ B,
uiff: uiff(P;Q),
rev_uimplies: rev_uimplies(P;Q)
Lemmas referenced :
req_witness,
subtype_rel_self,
int-to-real_wf,
meq_wf,
mfun_wf,
metric-on-subtype,
metric_wf,
istype-universe,
is-mfun_wf,
meq_functionality,
meq_weakening,
meq_inversion,
meq-same
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
lambdaFormation_alt,
cut,
introduction,
sqequalRule,
sqequalHypSubstitution,
lambdaEquality_alt,
dependent_functionElimination,
thin,
hypothesisEquality,
extract_by_obid,
isectElimination,
applyEquality,
setElimination,
rename,
hypothesis,
dependent_set_memberEquality_alt,
productElimination,
universeIsType,
instantiate,
universeEquality,
because_Cache,
natural_numberEquality,
independent_functionElimination,
functionIsTypeImplies,
inhabitedIsType,
dependent_pairFormation_alt,
functionIsType,
productIsType,
setEquality,
independent_isectElimination,
setIsType,
unionIsType,
functionExtensionality,
unionElimination,
equalityIstype,
equalityTransitivity,
equalitySymmetry,
independent_pairFormation
Latex:
\mforall{}[X:Type]. \mforall{}[dX:metric(X)]. \mforall{}[A,B:X {}\mrightarrow{} \mBbbP{}].
((\mforall{}x1,x2:X. (x1 \mequiv{} x2 {}\mRightarrow{} A[x1] {}\mRightarrow{} A[x2]))
{}\mRightarrow{} (\mforall{}x1,x2:X. (x1 \mequiv{} x2 {}\mRightarrow{} B[x1] {}\mRightarrow{} B[x2]))
{}\mRightarrow{} (\mforall{}x:X. (A[x] \mvee{} B[x]))
{}\mRightarrow{} (\mforall{}[Y:Type]. \mforall{}[dY:metric(Y)].
\mforall{}f:FUN(\{x:X| A[x]\} {}\mrightarrow{} Y). \mforall{}g:FUN(\{x:X| B[x]\} {}\mrightarrow{} Y).
\mexists{}h:FUN(X {}\mrightarrow{} Y). \mforall{}x:X. ((A[x] {}\mRightarrow{} h x \mequiv{} f x) \mwedge{} (B[x] {}\mRightarrow{} h x \mequiv{} g x))
supposing \mforall{}x:X. ((A[x] \mwedge{} B[x]) {}\mRightarrow{} f x \mequiv{} g x)))
Date html generated:
2019_10_30-AM-06_22_34
Last ObjectModification:
2019_10_02-AM-09_58_19
Theory : reals
Home
Index