---

Step * of 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])))
BY
{ Auto }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. ∀x,y:T.  Dec(R[x;y])
4. Linorder(T;x,y.R[x;y])
5. a : T
6. b : T
7. ¬strict_part(x,y.R[x;y];a;b)
⊢ R[b;a]

---

Latex:

---

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])))


By

---

Latex:
Auto

---

Home Index