---

Step * of Lemma weak-continuity-skolem_functionality

∀[T,S:Type].
  ∀e:T ~ S. ∀F:(ℕ ⟶ S) ⟶ ℕ.  (weak-continuity-skolem(T;λf.(F ((fst(e)) o f))) ⇒ weak-continuity-skolem(S;F))
BY
{ (RepeatFor 3 ((D 0 THENA Auto))
   THEN D -1
   THEN Reduce 0
   THEN Auto
   THEN (FLemma `biject-inverse` [-3] THENA Auto)
   THEN ExRepD
   THEN RenameVar `i' 3
   THEN RenameVar `j' (-3)
   THEN D -4) }

1
1. [T] : Type
2. [S] : Type
3. i : T ⟶ S
4. e1 : Bij(T;S;i)
5. F : (ℕ ⟶ S) ⟶ ℕ
6. M : (ℕ ⟶ T) ⟶ ℕ
7. ∀f,g:ℕ ⟶ T.  ((f = g ∈ (ℕM f ⟶ T)) ⇒ (((λf@0.(F (i o f@0))) f) = ((λf@0.(F (i o f@0))) g) ∈ ℕ))
8. j : S ⟶ T
9. ∀b:S. ((i (j b)) = b ∈ S)
10. ∀a:T. ((j (i a)) = a ∈ T)
⊢ weak-continuity-skolem(S;F)

---

Latex:

---

Latex:
\mforall{}[T,S:Type].
    \mforall{}e:T  \msim{}  S.  \mforall{}F:(\mBbbN{}  {}\mrightarrow{}  S)  {}\mrightarrow{}  \mBbbN{}.
        (weak-continuity-skolem(T;\mlambda{}f.(F  ((fst(e))  o  f)))  {}\mRightarrow{}  weak-continuity-skolem(S;F))


By

---

Latex:
(RepeatFor  3  ((D  0  THENA  Auto))
  THEN  D  -1
  THEN  Reduce  0
  THEN  Auto
  THEN  (FLemma  `biject-inverse`  [-3]  THENA  Auto)
  THEN  ExRepD
  THEN  RenameVar  `i'  3
  THEN  RenameVar  `j'  (-3)
  THEN  D  -4)

---

Home Index