Nuprl Lemma : unit-ball-approx_wf

[n,k:ℕ].  (unit-ball-approx(n;k) ∈ Type)


Proof




Definitions occuring in Statement :  unit-ball-approx: unit-ball-approx(n;k) nat: uall: [x:A]. B[x] member: t ∈ T universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T unit-ball-approx: unit-ball-approx(n;k) nat: so_lambda: λ2x.t[x] subtype_rel: A ⊆B int_seg: {i..j-} so_apply: x[s] prop:
Lemmas referenced :  int_seg_wf le_wf sum_wf istype-nat
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalRule setEquality functionEquality extract_by_obid sqequalHypSubstitution isectElimination thin natural_numberEquality setElimination rename hypothesisEquality hypothesis minusEquality addEquality because_Cache lambdaEquality_alt applyEquality inhabitedIsType equalityTransitivity equalitySymmetry universeIsType multiplyEquality axiomEquality isect_memberEquality_alt isectIsTypeImplies

Latex:
\mforall{}[n,k:\mBbbN{}].    (unit-ball-approx(n;k)  \mmember{}  Type)



Date html generated: 2019_10_30-AM-11_28_01
Last ObjectModification: 2019_06_28-PM-01_56_05

Theory : real!vectors


Home Index