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` 0 THEN Auto THEN RepeatFor 3 ((D 0 THENA Auto)))xxx }
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:
xxx(Unfold `so\_apply` 0 THEN Auto THEN RepeatFor 3 ((D 0 THENA Auto)))xxx
Home
Index