### Nuprl Lemma : linorder_lt_neg

[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
((∀x,y:T.  Dec(R[x;y]))  Linorder(T;x,y.R[x;y])  (∀a,b:T.  strict_part(x,y.R[x;y];a;b) ⇐⇒ R[b;a])))

Proof

Definitions occuring in Statement :  linorder: Linorder(T;x,y.R[x; y]) strict_part: strict_part(x,y.R[x; y];a;b) decidable: Dec(P) uall: [x:A]. B[x] prop: so_apply: x[s1;s2] all: x:A. B[x] iff: ⇐⇒ Q not: ¬A implies:  Q function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] implies:  Q all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q member: t ∈ T prop: so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] rev_implies:  Q not: ¬A false: False so_lambda: λ2x.t[x] so_apply: x[s] strict_part: strict_part(x,y.R[x; y];a;b) decidable: Dec(P) or: P ∨ Q linorder: Linorder(T;x,y.R[x; y]) connex: Connex(T;x,y.R[x; y]) order: Order(T;x,y.R[x; y]) anti_sym: AntiSym(T;x,y.R[x; y]) trans: Trans(T;x,y.E[x; y]) refl: Refl(T;x,y.E[x; y])
Lemmas referenced :  not_wf strict_part_wf linorder_wf all_wf decidable_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  lambdaFormation independent_pairFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality sqequalRule lambdaEquality applyEquality hypothesis independent_functionElimination voidElimination Error :functionIsType,  Error :universeIsType,  Error :inhabitedIsType,  universeEquality productElimination dependent_functionElimination unionElimination

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
((\mforall{}x,y:T.    Dec(R[x;y]))
{}\mRightarrow{}  Linorder(T;x,y.R[x;y])
{}\mRightarrow{}  (\mforall{}a,b:T.    (\mneg{}strict\_part(x,y.R[x;y];a;b)  \mLeftarrow{}{}\mRightarrow{}  R[b;a])))

Date html generated: 2019_06_20-PM-00_30_02
Last ObjectModification: 2018_09_26-PM-00_04_59

Theory : rel_1

Home Index