---

Step * 1 of Lemma parallel-classrel-weak


1. [T] : Type
2. [Info] : Type
3. [X] : EClass(T)
4. [Y] : EClass(T)
5. [es] : EO+(Info)
6. [e] : E
7. [v] : T
8. uiff(v ∈ X || Y(e);v ∈ X(e) ↓∨ v ∈ Y(e))
⊢ v ∈ X || Y(e) ⇐⇒ v ∈ X(e) ↓∨ v ∈ Y(e)
BY
{ Auto }

---

Latex:



1.  [T]  :  Type
2.  [Info]  :  Type
3.  [X]  :  EClass(T)
4.  [Y]  :  EClass(T)
5.  [es]  :  EO+(Info)
6.  [e]  :  E
7.  [v]  :  T
8.  uiff(v  \mmember{}  X  ||  Y(e);v  \mmember{}  X(e)  \mdownarrow{}\mvee{}  v  \mmember{}  Y(e))
\mvdash{}  v  \mmember{}  X  ||  Y(e)  \mLeftarrow{}{}\mRightarrow{}  v  \mmember{}  X(e)  \mdownarrow{}\mvee{}  v  \mmember{}  Y(e)


By

Auto

---

Home Index