Nuprl Lemma : m-ball-boundary
∀[X:Type]. ∀[d:metric(X)]. ∀[c:X]. ∀[r:ℝ].
m-boundary(X;d;m-ball(X;d;c;r)) ≡ m-sphere(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: ℕ+,
ext-eq: A ≡ B,
uimplies: b supposing a,
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,
ext-eq: A ≡ B,
and: P ∧ Q,
subtype_rel: A ⊆r B,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
prop: ℙ,
nat_plus: ℕ+,
rneq: x ≠ y,
guard: {T},
or: P ∨ Q,
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
implies: P ⇒ Q,
rless: x < y,
sq_exists: ∃x:A [B[x]],
decidable: Dec(P),
not: ¬A,
satisfiable_int_formula: satisfiable_int_formula(fmla),
false: False,
top: Top
Latex:
\mforall{}[X:Type]. \mforall{}[d:metric(X)]. \mforall{}[c:X]. \mforall{}[r:\mBbbR{}].
m-boundary(X;d;m-ball(X;d;c;r)) \mequiv{} m-sphere(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_48
Last ObjectModification:
2019_11_07-PM-00_32_15
Theory : reals
Home
Index