Nuprl Lemma : qmin_wf

[x,y:ℚ].  (qmin(x;y) ∈ ℚ)


Proof




Definitions occuring in Statement :  qmin: qmin(x;y) rationals: uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  qmin: qmin(x;y) uall: [x:A]. B[x] member: t ∈ T
Lemmas referenced :  ifthenelse_wf q_le_wf rationals_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality because_Cache

Latex:
\mforall{}[x,y:\mBbbQ{}].    (qmin(x;y)  \mmember{}  \mBbbQ{})



Date html generated: 2016_05_15-PM-10_43_13
Last ObjectModification: 2015_12_27-PM-07_56_12

Theory : rationals


Home Index