Nuprl Lemma : rleq_wf

[x,y:ℝ].  (x ≤ y ∈ ℙ)


Proof




Definitions occuring in Statement :  rleq: x ≤ y real: uall: [x:A]. B[x] prop: member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T rleq: x ≤ y subtype_rel: A ⊆B real:
Lemmas referenced :  rnonneg_wf rsub_wf real_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis applyEquality lambdaEquality setElimination rename because_Cache axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality

Latex:
\mforall{}[x,y:\mBbbR{}].    (x  \mleq{}  y  \mmember{}  \mBbbP{})



Date html generated: 2016_05_18-AM-07_04_35
Last ObjectModification: 2015_12_28-AM-00_35_31

Theory : reals


Home Index