Nuprl Lemma : qless_transitivity_2_qorder

[a,b,c:ℚ].  (a < c) supposing ((b ≤ c) and a < b)


Proof




Definitions occuring in Statement :  qle: r ≤ s qless: r < s rationals: uimplies: supposing a uall: [x:A]. B[x]
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T subtype_rel: A ⊆B qadd_grp: <ℚ+> grp_car: |g| pi1: fst(t) qless: r < s uimplies: supposing a grp_lt: a < b set_lt: a <b guard: {T} oset_of_ocmon: g↓oset dset_of_mon: g↓set set_car: |p| implies:  Q qle: r ≤ s grp_leq: a ≤ b infix_ap: y
Lemmas referenced :  grp_lt_transitivity_2 qadd_grp_wf2 ocgrp_subtype_ocmon assert_witness set_blt_wf oset_of_ocmon_wf0 mon_subtype_grp_sig dmon_subtype_mon abdmonoid_dmon ocmon_subtype_abdmonoid subtype_rel_transitivity ocgrp_wf ocmon_wf abdmonoid_wf dmon_wf mon_wf grp_sig_wf istype-assert grp_le_wf rationals_wf
Rules used in proof :  cut introduction extract_by_obid sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isectElimination thin hypothesis applyEquality sqequalRule isect_memberFormation_alt instantiate independent_isectElimination hypothesisEquality independent_functionElimination because_Cache isect_memberEquality_alt isectIsTypeImplies inhabitedIsType universeIsType

Latex:
\mforall{}[a,b,c:\mBbbQ{}].    (a  <  c)  supposing  ((b  \mleq{}  c)  and  a  <  b)



Date html generated: 2020_05_20-AM-09_14_37
Last ObjectModification: 2020_02_03-PM-02_48_17

Theory : rationals


Home Index