---

Step * of Lemma strong-continuity2-implies-3

∀[T:Type]. ∀[F:(ℕ ⟶ T) ⟶ ℕ].  (strong-continuity2(T;F) ⇒ strong-continuity3(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)) ∈ (ℕ?))) ∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (ℕ?) supposing ↑isl(M n f)))
⊢ ∃M:n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕ?)
   ∀f:ℕ ⟶ T. ∃n:ℕ. (((M n f) = (inl (F f)) ∈ (ℕ?)) ∧ (∀m:ℕ. ((↑isl(M m f)) ⇒ (m = n ∈ ℕ))))

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  D  -1  THEN  UnfoldTopAb  0)

---

Home Index