Nuprl Lemma : m-open-ball_wf
∀[X:Type]. ∀[d:metric(X)]. ∀[c:X]. ∀[r:ℝ]. (m-open-ball(X;d;c;r) ∈ Type)
Proof
Definitions occuring in Statement :
m-open-ball: m-open-ball(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-open-ball: m-open-ball(X;d;c;r),
prop: ℙ
Latex:
\mforall{}[X:Type]. \mforall{}[d:metric(X)]. \mforall{}[c:X]. \mforall{}[r:\mBbbR{}]. (m-open-ball(X;d;c;r) \mmember{} Type)
Date html generated:
2020_05_20-AM-11_46_10
Last ObjectModification:
2019_11_07-AM-10_28_04
Theory : reals
Home
Index