---

Step * of Lemma bag-dickson-lemma

∀p:ℕ. ∀[T:Type]. (T ~ ℕp ⇒ (∀A:ℕ ⟶ bag(T). ∃j:ℕ. ∃i:ℕj. sub-bag(T;A[i];A[j])))
BY
{ (Auto
   THEN D -2
   THEN (InstLemma `Dickson\'s lemma` [⌜p⌝;⌜λ2k i.#([x∈A[i]|(f x =z k)])⌝]⋅ THENA Auto)
   THEN RepeatFor 2 (ParallelLast)) }

1
1. p : ℕ
2. [T] : Type
3. f : T ⟶ ℕp
4. Bij(T;ℕp;f)
5. A : ℕ ⟶ bag(T)
6. j : ℕ
7. i : ℕj
8. ∀k:ℕp. (#([x∈A[i]|(f x =z k)]) ≤ #([x∈A[j]|(f x =z k)]))
⊢ sub-bag(T;A[i];A[j])

---

Latex:

---

Latex:
\mforall{}p:\mBbbN{}.  \mforall{}[T:Type].  (T  \msim{}  \mBbbN{}p  {}\mRightarrow{}  (\mforall{}A:\mBbbN{}  {}\mrightarrow{}  bag(T).  \mexists{}j:\mBbbN{}.  \mexists{}i:\mBbbN{}j.  sub-bag(T;A[i];A[j])))


By

---

Latex:
(Auto
  THEN  D  -2
  THEN  (InstLemma  `Dickson\mbackslash{}'s  lemma`  [\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}k  i.\#([x\mmember{}A[i]|(f  x  =\msubz{}  k)])\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (ParallelLast))

---

Home Index