Nuprl Lemma : ip-circle-circle
∀rv:InnerProductSpace. ∀a,b:Point. ∀c:{c:Point| a # c} . ∀d:Point.
∀[p:{p:Point| ab=ap ∧ cd ≥ cp} ]. ∀[q:{q:Point| cd=cq ∧ ab ≥ aq} ].
∃u:{u:Point| ab=au ∧ cd=cu} . (∃v:{Point| ((ab=av ∧ cd=cv) ∧ ((ab > aq ∧ cd > cp) ⇒ u # v))})
Proof
Definitions occuring in Statement :
ip-gt: cd > ab,
ip-ge: cd ≥ ab,
ip-congruent: ab=cd,
inner-product-space: InnerProductSpace,
ss-sep: x # y,
ss-point: Point,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
sq_exists: ∃x:{A| B[x]},
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
set: {x:A| B[x]}
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
uall: ∀[x:A]. B[x],
and: P ∧ Q,
cand: A c∧ B,
uiff: uiff(P;Q),
uimplies: b supposing a,
prop: ℙ,
subtype_rel: A ⊆r B,
exists: ∃x:A. B[x],
so_lambda: λ2x.t[x],
implies: P ⇒ Q,
so_apply: x[s],
guard: {T},
sq_exists: ∃x:{A| B[x]},
sq_stable: SqStable(P),
squash: ↓T
Lemmas referenced :
ip-circle-circle-lemma3,
ip-ge-iff,
ip-congruent_wf,
rleq_wf,
rv-norm_wf,
rv-sub_wf,
real_wf,
int-to-real_wf,
req_wf,
rmul_wf,
rv-ip_wf,
sq_exists_wf,
ip-gt_wf,
ss-sep_wf,
set_wf,
ip-ge_wf,
ss-point_wf,
real-vector-space_subtype1,
inner-product-space_subtype,
subtype_rel_transitivity,
inner-product-space_wf,
real-vector-space_wf,
separation-space_wf,
sq_stable__ip-congruent,
ip-gt-iff
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
hypothesis,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesisEquality,
isect_memberFormation,
isectElimination,
setElimination,
rename,
dependent_set_memberEquality,
productElimination,
independent_pairFormation,
because_Cache,
independent_isectElimination,
productEquality,
applyEquality,
sqequalRule,
lambdaEquality,
setEquality,
natural_numberEquality,
dependent_pairFormation,
functionEquality,
instantiate,
dependent_set_memberFormation,
independent_functionElimination,
imageMemberEquality,
baseClosed,
imageElimination
Latex:
\mforall{}rv:InnerProductSpace. \mforall{}a,b:Point. \mforall{}c:\{c:Point| a \# c\} . \mforall{}d:Point.
\mforall{}[p:\{p:Point| ab=ap \mwedge{} cd \mgeq{} cp\} ]. \mforall{}[q:\{q:Point| cd=cq \mwedge{} ab \mgeq{} aq\} ].
\mexists{}u:\{u:Point| ab=au \mwedge{} cd=cu\} . (\mexists{}v:\{Point| ((ab=av \mwedge{} cd=cv) \mwedge{} ((ab > aq \mwedge{} cd > cp) {}\mRightarrow{} u \# v))\})
Date html generated:
2017_10_05-AM-00_12_26
Last ObjectModification:
2017_03_21-AM-00_38_21
Theory : inner!product!spaces
Home
Index