Nuprl Lemma : m-ball-boundary-subtype-m-sphere
∀[X:Type]. ∀[d:metric(X)]. ∀[c:X]. ∀[r:ℝ]. (m-boundary(X;d;m-ball(X;d;c;r)) ⊆r m-sphere(X;d;c;r))
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),
metric: metric(X),
real: ℝ,
subtype_rel: A ⊆r B,
uall: ∀[x:A]. B[x],
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
subtype_rel: A ⊆r B,
m-boundary: m-boundary(X;d;A),
m-sphere: m-sphere(X;d;c;r),
m-ball: m-ball(X;d;c;r),
uimplies: b supposing a,
not: ¬A,
implies: P ⇒ Q,
rneq: x ≠ y,
or: P ∨ Q,
all: ∀x:A. B[x],
prop: ℙ,
m-interior-point: m-interior-point(X;d;A;p),
exists: ∃x:A. B[x],
nat_plus: ℕ+,
guard: {T},
iff: P ⇐⇒ Q,
and: 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),
false: False,
top: Top,
so_lambda: λ2x.t[x],
so_apply: x[s],
respects-equality: respects-equality(S;T),
uiff: uiff(P;Q),
req_int_terms: t1 ≡ t2,
rev_uimplies: rev_uimplies(P;Q),
rge: x ≥ y
Latex:
\mforall{}[X:Type]. \mforall{}[d:metric(X)]. \mforall{}[c:X]. \mforall{}[r:\mBbbR{}]. (m-boundary(X;d;m-ball(X;d;c;r)) \msubseteq{}r m-sphere(X;d;c;r))
Date html generated:
2020_05_20-AM-11_47_08
Last ObjectModification:
2019_11_07-AM-10_54_08
Theory : reals
Home
Index