Step
*
of Lemma
strong-continuity3-implies-4
No Annotations
∀[T:Type]. ∀F:(ℕ ⟶ T) ⟶ ℕ. (strong-continuity3(T;F)
⇒ strong-continuity4(T;F))
BY
{ (Auto THEN D -1 THEN UnfoldTopAb 0) }
1
1. [T] : Type
2. F : (ℕ ⟶ T) ⟶ ℕ
3. M : n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕ?)
4. ∀f:ℕ ⟶ T. ∃n:ℕ. (((M n f) = (inl (F f)) ∈ (ℕ?)) ∧ (∀m:ℕ. ((↑isl(M m f))
⇒ (m = n ∈ ℕ))))
⊢ ∃M:n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕn?)
∀f:ℕ ⟶ T. ∃n:ℕ. (((M n f) = (inl (F f)) ∈ (ℕ?)) ∧ (∀m:ℕ. ((↑isl(M m f))
⇒ ((M m f) = (inl (F f)) ∈ (ℕ?)))))
Latex:
Latex:
No Annotations
\mforall{}[T:Type]. \mforall{}F:(\mBbbN{} {}\mrightarrow{} T) {}\mrightarrow{} \mBbbN{}. (strong-continuity3(T;F) {}\mRightarrow{} strong-continuity4(T;F))
By
Latex:
(Auto THEN D -1 THEN UnfoldTopAb 0)
Home
Index