Nuprl Lemma : m-sphere_wf
∀[X:Type]. ∀[d:metric(X)]. ∀[c:X]. ∀[r:ℝ]. (m-sphere(X;d;c;r) ∈ Type)
Proof
Definitions occuring in Statement :
m-sphere: m-sphere(X;d;c;r),
metric: metric(X),
real: ℝ,
uall: ∀[x:A]. B[x],
member: t ∈ T,
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
m-sphere: m-sphere(X;d;c;r),
prop: ℙ
Latex:
\mforall{}[X:Type]. \mforall{}[d:metric(X)]. \mforall{}[c:X]. \mforall{}[r:\mBbbR{}]. (m-sphere(X;d;c;r) \mmember{} Type)
Date html generated:
2020_05_20-AM-11_46_48
Last ObjectModification:
2019_11_07-AM-10_29_57
Theory : reals
Home
Index