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
xxx(Unfold `so_apply` THEN Auto THEN RepeatFor ((D THENA Auto)))xxx }

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

2
.....subterm..... T:t
1:n
1. Type
2. T:Type ⟶ A ⟶ Type
3. ∀a:A. Continuous+(T.G a)
4. : ℕ ⟶ Type
5. x:A ⋂ (⋂n:ℕ(X n)) x
⊢ x ∈ ⋂n:ℕx:A ⋂ (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:
xxx(Unfold  `so\_apply`  0  THEN  Auto  THEN  RepeatFor  3  ((D  0  THENA  Auto)))xxx




Home Index