Nuprl Lemma : ocmon_connex

g:OCMon. ∀x,y:|g|.  ((↑(x ≤b y)) ∨ (↑(y ≤b x)))


Proof




Definitions occuring in Statement :  ocmon: OCMon grp_le: b grp_car: |g| assert: b infix_ap: y all: x:A. B[x] or: P ∨ Q
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T and: P ∧ Q ulinorder: UniformLinorder(T;x,y.R[x; y]) uorder: UniformOrder(T;x,y.R[x; y]) eqfun_p: IsEqFun(T;eq) monot: monot(T;x,y.R[x; y];f) cancel: Cancel(T;S;op) connex: Connex(T;x,y.R[x; y]) uanti_sym: UniformlyAntiSym(T;x,y.R[x; y]) utrans: UniformlyTrans(T;x,y.E[x; y]) urefl: UniformlyRefl(T;x,y.E[x; y])
Lemmas referenced :  ocmon_properties ocmon_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality hypothesis productElimination sqequalRule

Latex:
\mforall{}g:OCMon.  \mforall{}x,y:|g|.    ((\muparrow{}(x  \mleq{}\msubb{}  y))  \mvee{}  (\muparrow{}(y  \mleq{}\msubb{}  x)))



Date html generated: 2016_05_15-PM-00_11_21
Last ObjectModification: 2015_12_26-PM-11_43_31

Theory : groups_1


Home Index