---

Step * 1 1 1 of Lemma fix_wf_corec2'

.....wf..... 
1. F : Type ⟶ Type
2. H : Type ⟶ Type
3. Continuous(T.H[T])
4. G : ⋂T:{T:Type| corec(T.F[T]) ⊆r T} . (H[T] ⟶ H[F[T]]) ⋂ Top ⟶ H[Top]
5. n : ℤ
⊢ G ∈ Top ⟶ H[Top]
BY
{ (Isect2HD' 4 THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  F  :  Type  {}\mrightarrow{}  Type
2.  H  :  Type  {}\mrightarrow{}  Type
3.  Continuous(T.H[T])
4.  G  :  \mcap{}T:\{T:Type|  corec(T.F[T])  \msubseteq{}r  T\}  .  (H[T]  {}\mrightarrow{}  H[F[T]])  \mcap{}  Top  {}\mrightarrow{}  H[Top]
5.  n  :  \mBbbZ{}
\mvdash{}  G  \mmember{}  Top  {}\mrightarrow{}  H[Top]


By

---

Latex:
(Isect2HD'  4  THEN  Auto)

---

Home Index