Step
*
1
2
of Lemma
strong-continuous-list
1. F : Type ⟶ Type
2. Continuous+(T.F T)
3. X : ℕ ⟶ Type
4. x : ⋂n:ℕ. ((F (X n)) List)
5. ∀i:ℕ||x||. (x[i] ∈ F (⋂n:ℕ. (X n)))
⊢ x ∈ (F (⋂n:ℕ. (X n))) List
BY
{ xxx(Assert x ∈ (F (X 0)) List BY
(With ⌜0⌝ (DVar `x')⋅ THEN Auto))xxx }
1
1. F : Type ⟶ Type
2. Continuous+(T.F T)
3. X : ℕ ⟶ Type
4. x : ⋂n:ℕ. ((F (X n)) List)
5. ∀i:ℕ||x||. (x[i] ∈ F (⋂n:ℕ. (X n)))
6. x ∈ (F (X 0)) List
⊢ x ∈ (F (⋂n:ℕ. (X n))) List
Latex:
Latex:
1. F : Type {}\mrightarrow{} Type
2. Continuous+(T.F T)
3. X : \mBbbN{} {}\mrightarrow{} Type
4. x : \mcap{}n:\mBbbN{}. ((F (X n)) List)
5. \mforall{}i:\mBbbN{}||x||. (x[i] \mmember{} F (\mcap{}n:\mBbbN{}. (X n)))
\mvdash{} x \mmember{} (F (\mcap{}n:\mBbbN{}. (X n))) List
By
Latex:
xxx(Assert x \mmember{} (F (X 0)) List BY
(With \mkleeneopen{}0\mkleeneclose{} (DVar `x')\mcdot{} THEN Auto))xxx
Home
Index