---

Step * of Lemma xxconnex_iff_trichot

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  ((∀a,b:T.  Dec(R a b)) ⇒ (connex(T;R) ⇐⇒ {∀a,b:T.  (((R\) a b) ∨ ((R↔) a b) ∨ ((R\) b a))}))
BY
{ AssertLemma `connex_iff_trichot` [] }

1
1. ∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
     ((∀a,b:T.  Dec(R[a;b]))
     ⇒ (Connex(T;x,y.R[x;y])
        ⇐⇒ {∀a,b:T.  (strict_part(x,y.R[x;y];a;b) ∨ Symmetrize(x,y.R[x;y];a;b) ∨ strict_part(x,y.R[x;y];b;a))}))
⊢ ∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
    ((∀a,b:T.  Dec(R a b)) ⇒ (connex(T;R) ⇐⇒ {∀a,b:T.  (((R\) a b) ∨ ((R↔) a b) ∨ ((R\) b a))}))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}a,b:T.    Dec(R  a  b))  {}\mRightarrow{}  (connex(T;R)  \mLeftarrow{}{}\mRightarrow{}  \{\mforall{}a,b:T.    (((R\mbackslash{})  a  b)  \mvee{}  ((R\mrightleftharpoons{})  a  b)  \mvee{}  ((R\mbackslash{})  b  a))\}))


By

---

Latex:
AssertLemma  `connex\_iff\_trichot`  []

---

Home Index