---

Step * of Lemma strong-continuous-union

∀[F,G:Type ⟶ Type].  (Continuous+(T.F[T] + G[T])) supposing (Continuous+(T.G[T]) and Continuous+(T.F[T]))
BY
{ (Unfold `so_apply` 0 THEN Auto THEN Repeat ((D 0 THEN Auto))) }

1
.....subterm..... T:t
1:n
1. F : Type ⟶ Type
2. G : Type ⟶ Type
3. Continuous+(T.F T)
4. Continuous+(T.G T)
5. X : ℕ ⟶ Type
6. x : ⋂n:ℕ. (F (X n) + (G (X n)))
⊢ x ∈ F (⋂n:ℕ. (X n)) + (G (⋂n:ℕ. (X n)))

2
1. F : Type ⟶ Type
2. G : Type ⟶ Type
3. Continuous+(T.F T)
4. Continuous+(T.G T)
5. X : ℕ ⟶ Type
6. x : F (⋂n:ℕ. (X n)) + (G (⋂n:ℕ. (X n)))
7. n : ℕ
⊢ x ∈ F (X n) + (G (X n))

---

Latex:

---

Latex:
\mforall{}[F,G:Type  {}\mrightarrow{}  Type].
    (Continuous+(T.F[T]  +  G[T]))  supposing  (Continuous+(T.G[T])  and  Continuous+(T.F[T]))


By

---

Latex:
(Unfold  `so\_apply`  0  THEN  Auto  THEN  Repeat  ((D  0  THEN  Auto)))

---

Home Index