Nuprl Lemma : real-unit-ball_wf

[n:ℕ]. (B(n) ∈ Type)


Proof




Definitions occuring in Statement :  real-unit-ball: B(n) nat: uall: [x:A]. B[x] member: t ∈ T universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T real-unit-ball: B(n) prop:
Lemmas referenced :  real-vec_wf rleq_wf real-vec-norm_wf int-to-real_wf istype-nat
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalRule setEquality extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis natural_numberEquality axiomEquality equalityTransitivity equalitySymmetry

Latex:
\mforall{}[n:\mBbbN{}].  (B(n)  \mmember{}  Type)



Date html generated: 2019_10_30-AM-10_15_10
Last ObjectModification: 2019_06_28-PM-01_52_17

Theory : real!vectors


Home Index