---

Step * 1 1 of Lemma partial-type-continuous


1. X : ℕ ⟶ {T:Type| value-type(T)} 
2. a : Base
3. a ∈ ⋂n:ℕ. partial(X[n])
⊢ a ∈ partial(⋂n:ℕ. X[n])
BY
{ TACTIC:(MemTypeCD THEN Try (Complete (Auto))) }

1
.....wf..... 
1. X : ℕ ⟶ {T:Type| value-type(T)} 
2. a : Base
3. a ∈ ⋂n:ℕ. partial(X[n])
⊢ a ∈ base-partial(⋂n:ℕ. X[n])

2
.....antecedent..... 
1. X : ℕ ⟶ {T:Type| value-type(T)} 
2. a : Base
3. a ∈ ⋂n:ℕ. partial(X[n])
⊢ per-partial(⋂n:ℕ. X[n];a;a)

---

Latex:

---

Latex:

1.  X  :  \mBbbN{}  {}\mrightarrow{}  \{T:Type|  value-type(T)\} 
2.  a  :  Base
3.  a  \mmember{}  \mcap{}n:\mBbbN{}.  partial(X[n])
\mvdash{}  a  \mmember{}  partial(\mcap{}n:\mBbbN{}.  X[n])


By

---

Latex:
TACTIC:(MemTypeCD  THEN  Try  (Complete  (Auto)))

---

Home Index