---

Step * of Lemma linorder_le_neg

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (Linorder(T;x,y.R[x;y]) ⇒ (∀a,b:T.  (¬R[a;b] ⇐⇒ strict_part(x,y.R[x;y];b;a))))
BY
{ Auto }

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

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index