---

Step * of Lemma strong-continuity2-iff-3

∀[T:Type]. ∀[F:(ℕ ⟶ T) ⟶ ℕ].  (strong-continuity2(T;F) ⇐⇒ strong-continuity3(T;F))
BY
{ (EAuto 1 THEN All UnfoldTopAb THEN RepeatFor 2 (ParallelLast) THEN Auto THEN ExRepD) }

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 ∈ ℕ))))
5. f : ℕ ⟶ T
6. n2 : ℕ
7. (M n2 f) = (inl (F f)) ∈ (ℕ?)
8. ∀m:ℕ. ((↑isl(M m f)) ⇒ (m = n2 ∈ ℕ))
9. n1 : ℕ
10. (M n1 f) = (inl (F f)) ∈ (ℕ?)
11. n : ℕ
12. ↑isl(M n f)
⊢ (M n f) = (inl (F f)) ∈ (ℕ?)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[F:(\mBbbN{}  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbN{}].    (strong-continuity2(T;F)  \mLeftarrow{}{}\mRightarrow{}  strong-continuity3(T;F))


By

---

Latex:
(EAuto  1  THEN  All  UnfoldTopAb  THEN  RepeatFor  2  (ParallelLast)  THEN  Auto  THEN  ExRepD)

---

Home Index