---

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

∀F:(ℕ ⟶ 𝔹) ⟶ ℕ. ⇃(∃M:(ℕ ⟶ 𝔹) ⟶ ℕ. ∀f,g:ℕ ⟶ 𝔹.  ((f = g ∈ (ℕM f ⟶ 𝔹)) ⇒ ((F f) = (F g) ∈ ℕ)))
BY
{ ((UnivCD THENA Auto)
   THEN Fold `weak-continuity-skolem` 0
   THEN (Assert ℕ2 ~ 𝔹 BY
               EAuto 2)
   THEN RenameVar `e' (-1)
   THEN Assert ⌜⇃(weak-continuity-skolem(ℕ2;λf.(F ((fst(e)) o f))))⌝⋅) }

1
.....assertion..... 
1. F : (ℕ ⟶ 𝔹) ⟶ ℕ
2. e : ℕ2 ~ 𝔹
⊢ ⇃(weak-continuity-skolem(ℕ2;λf.(F ((fst(e)) o f))))

2
1. F : (ℕ ⟶ 𝔹) ⟶ ℕ
2. e : ℕ2 ~ 𝔹
3. ⇃(weak-continuity-skolem(ℕ2;λf.(F ((fst(e)) o f))))
⊢ ⇃(weak-continuity-skolem(𝔹;F))

---

Latex:

---

Latex:
\mforall{}F:(\mBbbN{}  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbN{}.  \00D9(\mexists{}M:(\mBbbN{}  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbN{}.  \mforall{}f,g:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.    ((f  =  g)  {}\mRightarrow{}  ((F  f)  =  (F  g))))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Fold  `weak-continuity-skolem`  0
  THEN  (Assert  \mBbbN{}2  \msim{}  \mBbbB{}  BY
                          EAuto  2)
  THEN  RenameVar  `e'  (-1)
  THEN  Assert  \mkleeneopen{}\00D9(weak-continuity-skolem(\mBbbN{}2;\mlambda{}f.(F  ((fst(e))  o  f))))\mkleeneclose{}\mcdot{})

---

Home Index