---

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


1. G : (ℕ ⟶ ℕ2) ⟶ ℕ
2. basic-strong-continuity(ℕ2;G)
⊢ weak-continuity-skolem(ℕ2;G)
BY
{ (InstLemma `basic-implies-strong-continuity2` [⌜ℕ2⌝;⌜G⌝]⋅ THEN Auto) }

1
1. G : (ℕ ⟶ ℕ2) ⟶ ℕ
2. basic-strong-continuity(ℕ2;G)
3. strong-continuity2(ℕ2;G)
⊢ weak-continuity-skolem(ℕ2;G)

---

Latex:

---

Latex:

1.  G  :  (\mBbbN{}  {}\mrightarrow{}  \mBbbN{}2)  {}\mrightarrow{}  \mBbbN{}
2.  basic-strong-continuity(\mBbbN{}2;G)
\mvdash{}  weak-continuity-skolem(\mBbbN{}2;G)


By

---

Latex:
(InstLemma  `basic-implies-strong-continuity2`  [\mkleeneopen{}\mBbbN{}2\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index