Nuprl Lemma : real-vec-sub_wf

[n:ℕ]. ∀[X,Y:ℝ^n].  (X Y ∈ ℝ^n)


Proof




Definitions occuring in Statement :  real-vec-sub: Y real-vec: ^n nat: uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  real-vec: ^n uall: [x:A]. B[x] member: t ∈ T real-vec-sub: Y nat:
Lemmas referenced :  rsub_wf int_seg_wf real_wf nat_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut lambdaEquality lemma_by_obid sqequalHypSubstitution isectElimination thin applyEquality hypothesisEquality hypothesis natural_numberEquality setElimination rename axiomEquality equalityTransitivity equalitySymmetry functionEquality isect_memberEquality because_Cache

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[X,Y:\mBbbR{}\^{}n].    (X  -  Y  \mmember{}  \mBbbR{}\^{}n)



Date html generated: 2016_05_18-AM-09_46_01
Last ObjectModification: 2015_12_27-PM-11_14_57

Theory : reals


Home Index