---

Step * of Lemma pairwise-iff2

No Annotations
∀[T:Type]
  ∀L:T List
    ∀[P:T ⟶ T ⟶ ℙ']
      ((∀x,y:T.  (P[x;y] ⇒ P[y;x]))
      ⇒ no_repeats(T;L)
      ⇒ ((∀x,y∈L.  P[x;y]) ⇐⇒ ∀x,y:T.  ((x ∈ L) ⇒ (y ∈ L) ⇒ (¬(x = y ∈ T)) ⇒ 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. no_repeats(T;L)
6. (∀x,y∈L.  P[x;y])
7. x : T
8. y : T
9. (x ∈ L)
10. (y ∈ L)
11. ¬(x = y ∈ T)
⊢ 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. no_repeats(T;L)
6. ∀x,y:T.  ((x ∈ L) ⇒ (y ∈ L) ⇒ (¬(x = y ∈ T)) ⇒ 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{}  no\_repeats(T;L)
            {}\mRightarrow{}  ((\mforall{}x,y\mmember{}L.    P[x;y])  \mLeftarrow{}{}\mRightarrow{}  \mforall{}x,y:T.    ((x  \mmember{}  L)  {}\mRightarrow{}  (y  \mmember{}  L)  {}\mRightarrow{}  (\mneg{}(x  =  y))  {}\mRightarrow{}  P[x;y])))


By

---

Latex:
Auto

---

Home Index