---

Step * of Lemma weak-continuity-equipollent

∀T:Type. (T ~ ℕ ⇒ (∀F:(ℕ ⟶ T) ⟶ ℕ. ∀f:ℕ ⟶ T.  ⇃(∃n:ℕ. ∀g:ℕ ⟶ T. ((f = g ∈ (ℕn ⟶ T)) ⇒ ((F f) = (F g) ∈ ℕ)))))
BY
{ ((UnivCD THENA Auto)
   THEN D 2
   THEN (RenameVar `m' 2 THEN (FLemma `biject-inverse` [3] THENA Auto) THEN ExRepD)
   THEN (InstLemma `strong-continuity2-implies-weak` [⌜λh.(F (g o h))⌝;⌜m o f⌝]⋅ THENA Auto)
   THEN Reduce -1
   THEN RepeatFor 2 ((ParallelLast THENA Auto))
   THEN Auto) }

1
1. T : Type
2. m : T ⟶ ℕ
3. Bij(T;ℕ;m)
4. F : (ℕ ⟶ T) ⟶ ℕ
5. f : ℕ ⟶ T
6. g : ℕ ⟶ T
7. ∀b:ℕ. ((m (g b)) = b ∈ ℕ)
8. ∀a:T. ((g (m a)) = a ∈ T)
9. n : ℕ
10. ∀g@0:ℕ ⟶ ℕ. (((m o f) = g@0 ∈ (ℕn ⟶ ℕ)) ⇒ ((F (g o (m o f))) = (F (g o g@0)) ∈ ℕ))
11. g1 : ℕ ⟶ T
12. f = g1 ∈ (ℕn ⟶ T)
⊢ (F f) = (F g1) ∈ ℕ

---

Latex:

---

Latex:
\mforall{}T:Type.  (T  \msim{}  \mBbbN{}  {}\mRightarrow{}  (\mforall{}F:(\mBbbN{}  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbN{}.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  T.    \00D9(\mexists{}n:\mBbbN{}.  \mforall{}g:\mBbbN{}  {}\mrightarrow{}  T.  ((f  =  g)  {}\mRightarrow{}  ((F  f)  =  (F  g))))))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  D  2
  THEN  (RenameVar  `m'  2  THEN  (FLemma  `biject-inverse`  [3]  THENA  Auto)  THEN  ExRepD)
  THEN  (InstLemma  `strong-continuity2-implies-weak`  [\mkleeneopen{}\mlambda{}h.(F  (g  o  h))\mkleeneclose{};\mkleeneopen{}m  o  f\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Reduce  -1
  THEN  RepeatFor  2  ((ParallelLast  THENA  Auto))
  THEN  Auto)

---

Home Index