Step
*
2
1
of Lemma
partial-type-continuous
1. X : ℕ ⟶ {T:Type| value-type(T)}
2. a : Base
3. b : Base
4. c : a = b ∈ (⋂n:ℕ. partial(X[n]))
5. ∀a:Base. ((a ∈ ⋂n:ℕ. partial(X[n]))
⇒ (a ∈ partial(⋂n:ℕ. X[n])))
⊢ a = b ∈ partial(⋂n:ℕ. X[n])
BY
{ (EqTypeCD THEN Auto) }
1
.....wf.....
1. X : ℕ ⟶ {T:Type| value-type(T)}
2. a : Base
3. b : Base
4. c : a = b ∈ (⋂n:ℕ. partial(X[n]))
5. ∀a:Base. ((a ∈ ⋂n:ℕ. partial(X[n]))
⇒ (a ∈ partial(⋂n:ℕ. X[n])))
⊢ a ∈ base-partial(⋂n:ℕ. X[n])
2
.....wf.....
1. X : ℕ ⟶ {T:Type| value-type(T)}
2. a : Base
3. b : Base
4. c : a = b ∈ (⋂n:ℕ. partial(X[n]))
5. ∀a:Base. ((a ∈ ⋂n:ℕ. partial(X[n]))
⇒ (a ∈ partial(⋂n:ℕ. X[n])))
⊢ b ∈ base-partial(⋂n:ℕ. X[n])
3
.....antecedent.....
1. X : ℕ ⟶ {T:Type| value-type(T)}
2. a : Base
3. b : Base
4. c : a = b ∈ (⋂n:ℕ. partial(X[n]))
5. ∀a:Base. ((a ∈ ⋂n:ℕ. partial(X[n]))
⇒ (a ∈ partial(⋂n:ℕ. X[n])))
⊢ per-partial(⋂n:ℕ. X[n];a;b)
Latex:
Latex:
1. X : \mBbbN{} {}\mrightarrow{} \{T:Type| value-type(T)\}
2. a : Base
3. b : Base
4. c : a = b
5. \mforall{}a:Base. ((a \mmember{} \mcap{}n:\mBbbN{}. partial(X[n])) {}\mRightarrow{} (a \mmember{} partial(\mcap{}n:\mBbbN{}. X[n])))
\mvdash{} a = b
By
Latex:
(EqTypeCD THEN Auto)
Home
Index