---

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