---

Step * of Lemma type-monotone-union-continuous

∀[F:Type ⟶ Type]. union-continuous{i:l}(T.F[T]) supposing Monotone(T.F[T])
BY
{ (Auto THEN RepeatFor 2 ((D 0 THEN Auto)) THEN Try ((BLemma `tunion_wf` THENA Auto))) }

1
.....subterm..... T:t
1:n
1. F : Type ⟶ Type
2. Monotone(T.F[T])
3. I : Type
4. X : I ⟶ Type
5. x : ⋃n:I.F[X n]@i
⊢ x ∈ F[⋃n:I.(X n)]

---

Latex:

---

Latex:
\mforall{}[F:Type  {}\mrightarrow{}  Type].  union-continuous\{i:l\}(T.F[T])  supposing  Monotone(T.F[T])


By

---

Latex:
(Auto  THEN  RepeatFor  2  ((D  0  THEN  Auto))  THEN  Try  ((BLemma  `tunion\_wf`  THENA  Auto)))

---

Home Index