---

Step * of Lemma strong-continuous-b-union

∀[F,G:Type ⟶ Type].
  (Continuous+(T.F[T] ⋃ G[T])) supposing ((∀T,S:Type.  (¬F[T] ⋂ G[S])) and 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. ∀T,S:Type.  (¬F T ⋂ G S)
6. X : ℕ ⟶ Type
7. x : ⋂n:ℕ. ((F (X n)) ⋃ (G (X n)))@i
⊢ 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. ∀T,S:Type.  (¬F T ⋂ G S)
6. X : ℕ ⟶ Type
7. x : (F (⋂n:ℕ. (X n))) ⋃ (G (⋂n:ℕ. (X n)))@i
8. n : ℕ
⊢ x ∈ (F (X n)) ⋃ (G (X n))

---

Latex:

---

Latex:
\mforall{}[F,G:Type  {}\mrightarrow{}  Type].
    (Continuous+(T.F[T]  \mcup{}  G[T]))  supposing 
          ((\mforall{}T,S:Type.    (\mneg{}F[T]  \mcap{}  G[S]))  and 
          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