---

Step * of Lemma basic-implies-strong-continuity2

No Annotations
∀[T:Type]. ∀[F:(ℕ ⟶ T) ⟶ ℕ].  (basic-strong-continuity(T;F) ⇒ strong-continuity2(T;F))
BY
{ (Auto THEN UnfoldTopAb (-1)) }

1
1. [T] : Type
2. [F] : (ℕ ⟶ T) ⟶ ℕ
3. ∃M:n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕ ⋃ (ℕ × ℕ)) [(∀f:ℕ ⟶ T
                                            ((∃n:ℕ. ((M n f) = (F f) ∈ ℕ))
                                            ∧ (∀n:ℕ. (M n f) = (F f) ∈ ℕ supposing M n f is an integer)
                                            ∧ (∀n,m:ℕ.  ((n ≤ m) ⇒ M n f is an integer ⇒ M m f is an integer))))]
⊢ strong-continuity2(T;F)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}[F:(\mBbbN{}  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbN{}].    (basic-strong-continuity(T;F)  {}\mRightarrow{}  strong-continuity2(T;F))


By

---

Latex:
(Auto  THEN  UnfoldTopAb  (-1))

---

Home Index