---

Step * 1 of Lemma strong-continuity2-implies-weak-skolem2

.....assertion..... 
1. F : (ℕ ⟶ 𝔹) ⟶ ℕ
2. e : ℕ2 ~ 𝔹
⊢ ⇃(weak-continuity-skolem(ℕ2;λf.(F ((fst(e)) o f))))
BY
{ ((GenConcl ⌜(λf.(F ((fst(e)) o f))) = G ∈ ((ℕ ⟶ ℕ2) ⟶ ℕ)⌝⋅ THENA Auto) THEN All Thin) }

1
1. G : (ℕ ⟶ ℕ2) ⟶ ℕ
⊢ ⇃(weak-continuity-skolem(ℕ2;G))

---

Latex:

---

Latex:
.....assertion..... 
1.  F  :  (\mBbbN{}  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbN{}
2.  e  :  \mBbbN{}2  \msim{}  \mBbbB{}
\mvdash{}  \00D9(weak-continuity-skolem(\mBbbN{}2;\mlambda{}f.(F  ((fst(e))  o  f))))


By

---

Latex:
((GenConcl  \mkleeneopen{}(\mlambda{}f.(F  ((fst(e))  o  f)))  =  G\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  All  Thin)

---

Home Index