---

Step * of Lemma general-cantor-to-int-uniform-continuity-half-squashed

No Annotations
∀B:ℕ ⟶ ℕ+. ∀F:(i:ℕ ⟶ ℕB[i]) ⟶ ℤ.  ⇃(∃n:ℕ. ∀f,g:i:ℕ ⟶ ℕB[i].  ((f = g ∈ (i:ℕn ⟶ ℕB[i])) ⇒ ((F f) = (F g) ∈ ℤ)))
BY
{ ((UnivCD THENA Auto) THEN BLemma `general-uniform-continuity-from-fan-ext` THEN Auto) }

1
1. B : ℕ ⟶ ℕ+
2. F : (i:ℕ ⟶ ℕB[i]) ⟶ ℤ
3. i : ℕ
⊢ ℕB[i]

2
1. B : ℕ ⟶ ℕ+
2. F : (i:ℕ ⟶ ℕB[i]) ⟶ ℤ
⊢ ⇃(∀i:ℕ. ∀K:ℕB[i] ⟶ ℕ.  (∃Bnd:ℕ [(∀t:ℕB[i]. ((K t) ≤ Bnd))]))

3
1. B : ℕ ⟶ ℕ+
2. F : (i:ℕ ⟶ ℕB[i]) ⟶ ℤ
⊢ ⇃(∃M:n:ℕ ⟶ (i:ℕn ⟶ ℕB[i]) ⟶ (ℤ?) [(∀f:i:ℕ ⟶ ℕB[i]
                                          ((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (ℤ?)))
                                          ∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (ℤ?) supposing ↑isl(M n f))))])

---

Latex:

---

Latex:
No  Annotations
\mforall{}B:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}\msupplus{}.  \mforall{}F:(i:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[i])  {}\mrightarrow{}  \mBbbZ{}.    \00D9(\mexists{}n:\mBbbN{}.  \mforall{}f,g:i:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[i].    ((f  =  g)  {}\mRightarrow{}  ((F  f)  =  (F  g))))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  BLemma  `general-uniform-continuity-from-fan-ext`  THEN  Auto)

---

Home Index