---

Step * 1 1 of Lemma weak-continuity-equipollent


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)
13. (F (g o (m o f))) = (F (g o (m o g1))) ∈ ℕ
⊢ (F f) = (F g1) ∈ ℕ
BY
{ (NthHypEq (-1) THEN RepeatFor 2 ((EqCD THEN Auto))) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  m  :  T  {}\mrightarrow{}  \mBbbN{}
3.  Bij(T;\mBbbN{};m)
4.  F  :  (\mBbbN{}  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbN{}
5.  f  :  \mBbbN{}  {}\mrightarrow{}  T
6.  g  :  \mBbbN{}  {}\mrightarrow{}  T
7.  \mforall{}b:\mBbbN{}.  ((m  (g  b))  =  b)
8.  \mforall{}a:T.  ((g  (m  a))  =  a)
9.  n  :  \mBbbN{}
10.  \mforall{}g@0:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  (((m  o  f)  =  g@0)  {}\mRightarrow{}  ((F  (g  o  (m  o  f)))  =  (F  (g  o  g@0))))
11.  g1  :  \mBbbN{}  {}\mrightarrow{}  T
12.  f  =  g1
13.  (F  (g  o  (m  o  f)))  =  (F  (g  o  (m  o  g1)))
\mvdash{}  (F  f)  =  (F  g1)


By

---

Latex:
(NthHypEq  (-1)  THEN  RepeatFor  2  ((EqCD  THEN  Auto)))

---

Home Index