---

Step * of Lemma urec-lfp

No Annotations
∀[f:Type ⟶ Type]. ⋂r:{r:Type| (f r) ⊆r r} . r ≡ urec(f) supposing continuous'-monotone{i:l}(T.f T)
BY
{ (Intros
   THEN (D 0 THEN Auto)
   THEN (D 0 THENA Auto)
   THEN Unfold `urec` (-1)
   THEN D_union (-1)
   THEN (DoSubsume THEN Auto)
   THEN (RepeatFor 2 (Thin (-1)) THEN NatInd (-1))) }

1
.....basecase..... 
1. f : Type ⟶ Type
2. continuous'-monotone{i:l}(T.f T)
3. n : ℤ
⊢ (f^0 Void) ⊆r (⋂r:{r:Type| (f r) ⊆r r} . r)

2
.....upcase..... 
1. f : Type ⟶ Type
2. continuous'-monotone{i:l}(T.f T)
3. n : ℤ
4. 0 < n
5. (f^n - 1 Void) ⊆r (⋂r:{r:Type| (f r) ⊆r r} . r)
⊢ (f^n Void) ⊆r (⋂r:{r:Type| (f r) ⊆r r} . r)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[f:Type  {}\mrightarrow{}  Type].  \mcap{}r:\{r:Type|  (f  r)  \msubseteq{}r  r\}  .  r  \mequiv{}  urec(f)  supposing  continuous'-monotone\{i:l\}(T.f  T)


By

---

Latex:
(Intros
  THEN  (D  0  THEN  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  Unfold  `urec`  (-1)
  THEN  D\_union  (-1)
  THEN  (DoSubsume  THEN  Auto)
  THEN  (RepeatFor  2  (Thin  (-1))  THEN  NatInd  (-1)))

---

Home Index