---

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


1. F : (ℕ ⟶ 𝔹) ⟶ ℕ
2. e : ℕ2 ~ 𝔹
3. ⇃(weak-continuity-skolem(ℕ2;λf.(F ((fst(e)) o f))))
⊢ ⇃(weak-continuity-skolem(𝔹;F))
BY
{ (MoveToConcl (-1)
   THEN BLemma `implies-quotient-true`
   THEN Auto
   THEN FLemma `weak-continuity-skolem_functionality` [-1]
   THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(MoveToConcl  (-1)
  THEN  BLemma  `implies-quotient-true`
  THEN  Auto
  THEN  FLemma  `weak-continuity-skolem\_functionality`  [-1]
  THEN  Auto)

---

Home Index