Nuprl Lemma : grp_leq_complement

[g:OCMon]. ∀[a,b:|g|].  uiff(¬(a ≤ b);b < a)


Proof




Definitions occuring in Statement :  grp_lt: a < b grp_leq: a ≤ b ocmon: OCMon grp_car: |g| uiff: uiff(P;Q) uall: [x:A]. B[x] not: ¬A
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T subtype_rel: A ⊆B ocmon: OCMon omon: OMon so_lambda: λ2x.t[x] prop: and: P ∧ Q abmonoid: AbMon mon: Mon so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt band: p ∧b q ifthenelse: if then else fi  uiff: uiff(P;Q) uimplies: supposing a bfalse: ff infix_ap: y so_apply: x[s] cand: c∧ B oset_of_ocmon: g↓oset dset_of_mon: g↓set set_car: |p| pi1: fst(t) set_leq: a ≤ b set_le: b pi2: snd(t) grp_leq: a ≤ b grp_lt: a < b set_lt: a <b not: ¬A false: False
Lemmas referenced :  set_leq_complement oset_of_ocmon_wf subtype_rel_sets abmonoid_wf ulinorder_wf grp_car_wf assert_wf infix_ap_wf bool_wf grp_le_wf equal_wf grp_eq_wf eqtt_to_assert cancel_wf grp_op_wf uall_wf monot_wf assert_witness set_blt_wf oset_of_ocmon_wf0 not_wf grp_leq_wf grp_lt_wf ocmon_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality applyEquality sqequalRule instantiate hypothesis because_Cache lambdaEquality productEquality setElimination rename cumulativity universeEquality functionEquality lambdaFormation unionElimination equalityElimination productElimination independent_isectElimination equalityTransitivity equalitySymmetry dependent_functionElimination independent_functionElimination setEquality independent_pairFormation isect_memberEquality independent_pairEquality voidElimination

Latex:
\mforall{}[g:OCMon].  \mforall{}[a,b:|g|].    uiff(\mneg{}(a  \mleq{}  b);b  <  a)



Date html generated: 2017_10_01-AM-08_14_58
Last ObjectModification: 2017_02_28-PM-01_59_47

Theory : groups_1


Home Index