---

Step * 1 of Lemma xxconnex_iff_trichot


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))}))
BY
{ Eval ``so_apply strict_part symmetrize`` 1 
THEN Eval ``xxconnex s_part sym_cl`` 0 
THEN Trivial }

---

Latex:

---

Latex:

1.  \mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
          ((\mforall{}a,b:T.    Dec(R[a;b]))
          {}\mRightarrow{}  (Connex(T;x,y.R[x;y])
                \mLeftarrow{}{}\mRightarrow{}  \{\mforall{}a,b:T.
                              (strict\_part(x,y.R[x;y];a;b)
                              \mvee{}  Symmetrize(x,y.R[x;y];a;b)
                              \mvee{}  strict\_part(x,y.R[x;y];b;a))\}))
\mvdash{}  \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:
Eval  ``so\_apply  strict\_part  symmetrize``  1 
THEN  Eval  ``xxconnex  s\_part  sym\_cl``  0 
THEN  Trivial

---

Home Index