---

Step * 1 of Lemma type-monotone-union-continuous

.....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)]
BY
{ (D_union (-1) THEN DoSubsume THEN Auto THEN All (Unfold `so_apply`)) }

1
1. F : Type ⟶ Type
2. Monotone(T.F T)
3. I : Type
4. X : I ⟶ Type
5. n : I@i
6. F (X n)@i
7. %2 = %2 ∈ (F (X n))
8. x : F (X n)@i
⊢ x ∈ F ⋃n:I.(X n)

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  F  :  Type  {}\mrightarrow{}  Type
2.  Monotone(T.F[T])
3.  I  :  Type
4.  X  :  I  {}\mrightarrow{}  Type
5.  x  :  \mcup{}n:I.F[X  n]@i
\mvdash{}  x  \mmember{}  F[\mcup{}n:I.(X  n)]


By

---

Latex:
(D\_union  (-1)  THEN  DoSubsume  THEN  Auto  THEN  All  (Unfold  `so\_apply`))

---

Home Index