---

Step * of Lemma dlattice-order-iff

∀[X:Type]. ∀as,bs:X List List.  (as ⇒ bs ⇐⇒ ∀x:X List. ((x ∈ bs) ⇒ (∃y:X List. ((y ∈ as) ∧ l_subset(X;y;x)))))
BY
{ Auto }

1
1. [X] : Type
2. as : X List List
3. bs : X List List
4. as ⇒ bs
5. x : X List
6. (x ∈ bs)
⊢ ∃y:X List. ((y ∈ as) ∧ l_subset(X;y;x))

2
1. [X] : Type
2. as : X List List
3. bs : X List List
4. ∀x:X List. ((x ∈ bs) ⇒ (∃y:X List. ((y ∈ as) ∧ l_subset(X;y;x))))
⊢ as ⇒ bs

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}as,bs:X  List  List.
        (as  {}\mRightarrow{}  bs  \mLeftarrow{}{}\mRightarrow{}  \mforall{}x:X  List.  ((x  \mmember{}  bs)  {}\mRightarrow{}  (\mexists{}y:X  List.  ((y  \mmember{}  as)  \mwedge{}  l\_subset(X;y;x)))))


By

---

Latex:
Auto

---

Home Index