---

Step * of Lemma member-concat-mklist

∀[T:Type]. ∀n:ℕ. ∀f:ℕn ⟶ (T List). ∀x:T.  ((x ∈ concat(mklist(n;f))) ⇐⇒ ∃i:ℕn. (x ∈ f i))
BY
{ (xxxIntrosxxx THEN RWO "member-concat" 0 THEN Auto THEN ExRepD) }

1
1. [T] : Type
2. n : ℕ
3. f : ℕn ⟶ (T List)
4. x : T
5. l : T List
6. (l ∈ mklist(n;f))
7. (x ∈ l)
⊢ ∃i:ℕn. (x ∈ f i)

2
1. [T] : Type
2. n : ℕ
3. f : ℕn ⟶ (T List)
4. x : T
5. i : ℕn
6. (x ∈ f i)
⊢ ∃l:T List. ((l ∈ mklist(n;f)) ∧ (x ∈ l))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}n:\mBbbN{}.  \mforall{}f:\mBbbN{}n  {}\mrightarrow{}  (T  List).  \mforall{}x:T.    ((x  \mmember{}  concat(mklist(n;f)))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}i:\mBbbN{}n.  (x  \mmember{}  f  i))


By

---

Latex:
(xxxIntrosxxx  THEN  RWO  "member-concat"  0  THEN  Auto  THEN  ExRepD)

---

Home Index