Nuprl Lemma : sq_stable_qle

[r,s:ℚ].  SqStable(r ≤ s)


Proof




Definitions occuring in Statement :  qle: r ≤ s rationals: sq_stable: SqStable(P) uall: [x:A]. B[x]
Definitions unfolded in proof :  qle: r ≤ s uall: [x:A]. B[x] member: t ∈ T subtype_rel: A ⊆B ocgrp: OGrp ocmon: OCMon abmonoid: AbMon mon: Mon qadd_grp: <ℚ+> grp_car: |g| pi1: fst(t) sq_stable: SqStable(P) implies:  Q grp_leq: a ≤ b infix_ap: y prop:
Lemmas referenced :  sq_stable__grp_leq qadd_grp_wf2 ocgrp_wf assert_witness grp_le_wf squash_wf grp_leq_wf rationals_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesis applyEquality lambdaEquality setElimination rename hypothesisEquality dependent_functionElimination because_Cache independent_functionElimination isect_memberEquality

Latex:
\mforall{}[r,s:\mBbbQ{}].    SqStable(r  \mleq{}  s)



Date html generated: 2016_05_15-PM-10_45_28
Last ObjectModification: 2015_12_27-PM-07_53_30

Theory : rationals


Home Index