---

Step * of Lemma generic-countable-intersection

∀[T:Type]. ∀[S:ℕ ⟶ (ℕ ⟶ T) ⟶ ℙ'].  ((∀i:ℕ. Generic{x:ℕ⟶T|S[i;x]}) ⇒ Generic{x:ℕ⟶T|∀i:ℕ. S[i;x]})
BY
{ xxx(xxxAutoxxx THEN (All (Unfold `generic`)))xxx }

1
1. [T] : Type
2. [S] : ℕ ⟶ (ℕ ⟶ T) ⟶ ℙ'
3. ∀i:ℕ
     ∃R:ℕ ⟶ (T List) ⟶ ℙ
      ((∀i:ℕ. ∀s:T List.  ∃s':T List. (s ≤ s' ∧ (R i s')))
      ∧ (∀x:ℕ ⟶ T. ((∀i:ℕ. ∃s:T List. ((R i s) ∧ (∀n:ℕ||s||. (s[n] = (x n) ∈ T)))) ⇒ S[i;x])))
⊢ ∃R:ℕ ⟶ (T List) ⟶ ℙ
   ((∀i:ℕ. ∀s:T List.  ∃s':T List. (s ≤ s' ∧ (R i s')))
   ∧ (∀x:ℕ ⟶ T. ((∀i:ℕ. ∃s:T List. ((R i s) ∧ (∀n:ℕ||s||. (s[n] = (x n) ∈ T)))) ⇒ (∀i:ℕ. S[i;x]))))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[S:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbP{}'].
    ((\mforall{}i:\mBbbN{}.  Generic\{x:\mBbbN{}{}\mrightarrow{}T|S[i;x]\})  {}\mRightarrow{}  Generic\{x:\mBbbN{}{}\mrightarrow{}T|\mforall{}i:\mBbbN{}.  S[i;x]\})


By

---

Latex:
xxx(xxxAutoxxx  THEN  (All  (Unfold  `generic`)))xxx

---

Home Index