---

Step * of Lemma generic-non-empty

No Annotations
∀[T:Type]. ∀[S:(ℕ ⟶ T) ⟶ ℙ'].  (T ⇒ Generic{f:ℕ⟶T|S[f]} ⇒ (∃f:ℕ ⟶ T. S[f]))
BY
{ (TACTIC:Auto THEN D -1 THEN Auto) }

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

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}[S:(\mBbbN{}  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbP{}'].    (T  {}\mRightarrow{}  Generic\{f:\mBbbN{}{}\mrightarrow{}T|S[f]\}  {}\mRightarrow{}  (\mexists{}f:\mBbbN{}  {}\mrightarrow{}  T.  S[f]))


By

---

Latex:
(TACTIC:Auto  THEN  D  -1  THEN  Auto)

---

Home Index