---

Step * 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)
⊢ (F f) = (F g1) ∈ ℕ
BY
{ (InstHyp [⌜m o g1⌝] (-3)⋅ 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)
13. (F (g o (m o f))) = (F (g o (m o g1))) ∈ ℕ
⊢ (F f) = (F g1) ∈ ℕ

---

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
\mvdash{}  (F  f)  =  (F  g1)


By

---

Latex:
(InstHyp  [\mkleeneopen{}m  o  g1\mkleeneclose{}]  (-3)\mcdot{}  THEN  Auto)

---

Home Index