Nuprl Lemma : m-sphere-subtype-m-ball-boundary
∀[X:Type]. ∀[d:metric(X)]. ∀[c:X]. ∀[r:ℝ].
m-sphere(X;d;c;r) ⊆r m-boundary(X;d;m-ball(X;d;c;r))
supposing ∀c,x:X. ∀M:ℕ+.
∃y:X. ((mdist(d;c;y) = (mdist(d;c;x) + mdist(d;x;y))) ∧ (r0 < mdist(d;y;x)) ∧ (mdist(d;y;x) ≤ (r1/r(M))))
Proof
Definitions occuring in Statement :
m-sphere: m-sphere(X;d;c;r),
m-ball: m-ball(X;d;c;r),
m-boundary: m-boundary(X;d;A),
mdist: mdist(d;x;y),
metric: metric(X),
rdiv: (x/y),
rleq: x ≤ y,
rless: x < y,
req: x = y,
radd: a + b,
int-to-real: r(n),
real: ℝ,
nat_plus: ℕ+,
uimplies: b supposing a,
subtype_rel: A ⊆r B,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
and: P ∧ Q,
natural_number: $n,
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
subtype_rel: A ⊆r B,
m-sphere: m-sphere(X;d;c;r),
m-boundary: m-boundary(X;d;A),
guard: {T},
m-ball: m-ball(X;d;c;r),
prop: ℙ,
not: ¬A,
implies: P ⇒ Q,
m-interior-point: m-interior-point(X;d;A;p),
exists: ∃x:A. B[x],
all: ∀x:A. B[x],
and: P ∧ Q,
squash: ↓T,
false: False,
so_lambda: λ2x.t[x],
so_apply: x[s],
nat_plus: ℕ+,
rneq: x ≠ y,
or: P ∨ Q,
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
rless: x < y,
sq_exists: ∃x:A [B[x]],
decidable: Dec(P),
satisfiable_int_formula: satisfiable_int_formula(fmla),
top: Top,
uiff: uiff(P;Q),
req_int_terms: t1 ≡ t2
Latex:
\mforall{}[X:Type]. \mforall{}[d:metric(X)]. \mforall{}[c:X]. \mforall{}[r:\mBbbR{}].
m-sphere(X;d;c;r) \msubseteq{}r m-boundary(X;d;m-ball(X;d;c;r))
supposing \mforall{}c,x:X. \mforall{}M:\mBbbN{}\msupplus{}.
\mexists{}y:X
((mdist(d;c;y) = (mdist(d;c;x) + mdist(d;x;y)))
\mwedge{} (r0 < mdist(d;y;x))
\mwedge{} (mdist(d;y;x) \mleq{} (r1/r(M))))
Date html generated:
2020_05_20-AM-11_47_28
Last ObjectModification:
2019_11_07-PM-00_30_17
Theory : reals
Home
Index