---

Step * of Lemma strong-continuity2-weak-skolem

∀[T:Type]. ∀[F:(ℕ ⟶ T) ⟶ ℕ].  (strong-continuity2(T;F) ⇒ weak-continuity-skolem(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:(ℕ ⟶ T) ⟶ ℕ. ∀f,g:ℕ ⟶ T.  ((f = g ∈ (ℕM f ⟶ T)) ⇒ ((F f) = (F g) ∈ ℕ))

---

Latex:

---

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


By

---

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

---

Home Index