Nuprl Lemma : real-cube_wf

[k:ℕ]. (real-cube(k) ∈ Type)


Proof




Definitions occuring in Statement :  real-cube: real-cube(k) nat: uall: [x:A]. B[x] member: t ∈ T universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T real-cube: real-cube(k)
Lemmas referenced :  real-vec_wf istype-nat
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalRule productEquality extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis axiomEquality equalityTransitivity equalitySymmetry

Latex:
\mforall{}[k:\mBbbN{}].  (real-cube(k)  \mmember{}  Type)



Date html generated: 2019_10_30-AM-11_30_58
Last ObjectModification: 2019_09_27-PM-00_41_55

Theory : real!vectors


Home Index