Step
*
of Lemma
pairwise-iff
No Annotations
∀[T:Type]
  ∀L:T List
    ∀[P:T ⟶ T ⟶ ℙ']
      ((∀x,y:T.  (P[x;y] 
⇒ P[y;x]))
      
⇒ (∀x:T. P[x;x])
      
⇒ ((∀x,y∈L.  P[x;y]) 
⇐⇒ ∀x,y:T.  ((x ∈ L) 
⇒ (y ∈ L) 
⇒ P[x;y])))
BY
{ Auto }
1
1. [T] : Type
2. L : T List
3. [P] : T ⟶ T ⟶ ℙ'
4. ∀x,y:T.  (P[x;y] 
⇒ P[y;x])
5. ∀x:T. P[x;x]
6. (∀x,y∈L.  P[x;y])
7. x : T
8. y : T
9. (x ∈ L)
10. (y ∈ L)
⊢ P[x;y]
2
1. [T] : Type
2. L : T List
3. [P] : T ⟶ T ⟶ ℙ'
4. ∀x,y:T.  (P[x;y] 
⇒ P[y;x])
5. ∀x:T. P[x;x]
6. ∀x,y:T.  ((x ∈ L) 
⇒ (y ∈ L) 
⇒ P[x;y])
⊢ (∀x,y∈L.  P[x;y])
Latex:
Latex:
No  Annotations
\mforall{}[T:Type]
    \mforall{}L:T  List
        \mforall{}[P:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}']
            ((\mforall{}x,y:T.    (P[x;y]  {}\mRightarrow{}  P[y;x]))
            {}\mRightarrow{}  (\mforall{}x:T.  P[x;x])
            {}\mRightarrow{}  ((\mforall{}x,y\mmember{}L.    P[x;y])  \mLeftarrow{}{}\mRightarrow{}  \mforall{}x,y:T.    ((x  \mmember{}  L)  {}\mRightarrow{}  (y  \mmember{}  L)  {}\mRightarrow{}  P[x;y])))
By
Latex:
Auto
Home
Index