---

Step * of Lemma fix_wf_corec_partial_nat

∀[F:Type ⟶ Type]
  ∀[f:⋂T:Type. ((T ⟶ partial(ℕ)) ⟶ F[T] ⟶ partial(ℕ))]. (fix(f) ∈ corec(T.F[T]) ⟶ partial(ℕ)) 
  supposing ContinuousMonotone(T.F[T])
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[F:Type  {}\mrightarrow{}  Type]
    \mforall{}[f:\mcap{}T:Type.  ((T  {}\mrightarrow{}  partial(\mBbbN{}))  {}\mrightarrow{}  F[T]  {}\mrightarrow{}  partial(\mBbbN{}))].  (fix(f)  \mmember{}  corec(T.F[T])  {}\mrightarrow{}  partial(\mBbbN{})) 
    supposing  ContinuousMonotone(T.F[T])


By

---

Latex:
Auto

---

Home Index