---

Step * of Lemma strong-continuous-dep-isect

∀A:Type. ∀G:T:Type ⟶ A ⟶ Type.  ((∀a:A. Continuous+(T.G[T;a])) ⇒ Continuous+(T.x:A ⋂ G[T;x]))
BY
{ TACTIC:(Unfold `so_apply` 0 THEN Auto THEN RepeatFor 3 ((D 0 THENA Auto))) }

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

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

---

Latex:

---

Latex:
\mforall{}A:Type.  \mforall{}G:T:Type  {}\mrightarrow{}  A  {}\mrightarrow{}  Type.    ((\mforall{}a:A.  Continuous+(T.G[T;a]))  {}\mRightarrow{}  Continuous+(T.x:A  \mcap{}  G[T;x]))


By

---

Latex:
TACTIC:(Unfold  `so\_apply`  0  THEN  Auto  THEN  RepeatFor  3  ((D  0  THENA  Auto)))

---

Home Index