Nuprl Lemma : oal_le_is_order

s:LOSet. ∀g:OGrp.  Order(|oal(s;g)|;ps,qs.ps ≤{s,g} qs)


Proof




Definitions occuring in Statement :  oal_le: ps ≤{s,g} qs oalist: oal(a;b) order: Order(T;x,y.R[x; y]) all: x:A. B[x] ocgrp: OGrp loset: LOSet set_car: |p|
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T ab_binrel: x,y:T. E[x; y] uall: [x:A]. B[x] subtype_rel: A ⊆B guard: {T} uimplies: supposing a so_lambda: λ2y.t[x; y] prop: so_apply: x[s1;s2] iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q implies:  Q ocgrp: OGrp xxirrefl: irrefl(T;R) xxtrans: trans(T;E)
Lemmas referenced :  ocgrp_wf loset_wf xxorder_eq_order set_car_wf oalist_wf ocmon_subtype_abdmonoid ocgrp_subtype_ocmon subtype_rel_transitivity ocmon_wf abdmonoid_wf ab_binrel_wf oal_le_wf ocgrp_subtype_abdgrp iff_weakening_equal xxorder_functionality_wrt_breqv refl_cl_wf oal_lt_wf oal_le_char refl_cl_is_order oal_lt_irrefl oal_lt_trans
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut lemma_by_obid hypothesis sqequalRule sqequalHypSubstitution isectElimination thin dependent_functionElimination hypothesisEquality applyEquality instantiate independent_isectElimination because_Cache lambdaEquality cumulativity universeEquality equalitySymmetry equalityTransitivity productElimination independent_functionElimination setElimination rename

Latex:
\mforall{}s:LOSet.  \mforall{}g:OGrp.    Order(|oal(s;g)|;ps,qs.ps  \mleq{}\{s,g\}  qs)



Date html generated: 2016_05_16-AM-08_21_40
Last ObjectModification: 2015_12_28-PM-06_25_20

Theory : polynom_2


Home Index