---

Step * of Lemma strong-continuous-isect2

∀[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 THENA Auto))
   THEN (Try (((MemTypeCD THENA Auto) THEN Isect2HD (-2)⋅)) THEN Isect2CD)⋅) }

1
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)@i
⊢ x ∈ F (⋂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 : ⋂n:ℕ. F (X n) ⋂ G (X n)@i
⊢ x ∈ G (⋂n:ℕ. (X n))

3
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))@i
7. n : ℕ
8. x ∈ G (⋂n:ℕ. (X n))
9. x ∈ F (⋂n:ℕ. (X n))
⊢ x ∈ F (X n)

4
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))@i
7. n : ℕ
8. x ∈ G (⋂n:ℕ. (X n))
9. x ∈ F (⋂n:ℕ. (X n))
⊢ x ∈ G (X n)

---

Latex:

---

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


By

---

Latex:
(Unfold  `so\_apply`  0
  THEN  Auto
  THEN  Repeat  ((D  0  THENA  Auto))
  THEN  (Try  (((MemTypeCD  THENA  Auto)  THEN  Isect2HD  (-2)\mcdot{}))  THEN  Isect2CD)\mcdot{})

---

Home Index