---

Step * 4 of Lemma general-uniform-continuity-from-fan


1. [B] : ℕ ⟶ Type
2. [%] : ∀i:ℕ. (B i)
3. ∀i:ℕ. ∀K:(B i) ⟶ ℕ.  (∃Bnd:ℕ [(∀t:B i. ((K t) ≤ Bnd))])
4. [T] : Type
5. F : (i:ℕ ⟶ (B i)) ⟶ T
6. M : n:ℕ ⟶ (i:ℕn ⟶ (B i)) ⟶ (T?)
7. [%5] : ∀f:i:ℕ ⟶ (B i)
            ((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (T?))) ∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (T?) supposing ↑isl(M n f)))
8. ∃k:ℕ [(∀f:i:ℕ ⟶ (B i). ∃n:ℕk. (↑isl(M n f)))]
⊢ ∃n:ℕ. ∀f,g:i:ℕ ⟶ (B i).  ((f = g ∈ (i:ℕn ⟶ (B i))) ⇒ ((F f) = (F g) ∈ T))
BY
{ ExRepD }

1
1. [B] : ℕ ⟶ Type
2. [%] : ∀i:ℕ. (B i)
3. ∀i:ℕ. ∀K:(B i) ⟶ ℕ.  (∃Bnd:ℕ [(∀t:B i. ((K t) ≤ Bnd))])
4. [T] : Type
5. F : (i:ℕ ⟶ (B i)) ⟶ T
6. M : n:ℕ ⟶ (i:ℕn ⟶ (B i)) ⟶ (T?)
7. [%5] : ∀f:i:ℕ ⟶ (B i)
            ((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (T?))) ∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (T?) supposing ↑isl(M n f)))
8. k : ℕ
9. ∀f:i:ℕ ⟶ (B i). ∃n:ℕk. (↑isl(M n f))
⊢ ∃n:ℕ. ∀f,g:i:ℕ ⟶ (B i).  ((f = g ∈ (i:ℕn ⟶ (B i))) ⇒ ((F f) = (F g) ∈ T))

---

Latex:

---

Latex:

1.  [B]  :  \mBbbN{}  {}\mrightarrow{}  Type
2.  [\%]  :  \mforall{}i:\mBbbN{}.  (B  i)
3.  \mforall{}i:\mBbbN{}.  \mforall{}K:(B  i)  {}\mrightarrow{}  \mBbbN{}.    (\mexists{}Bnd:\mBbbN{}  [(\mforall{}t:B  i.  ((K  t)  \mleq{}  Bnd))])
4.  [T]  :  Type
5.  F  :  (i:\mBbbN{}  {}\mrightarrow{}  (B  i))  {}\mrightarrow{}  T
6.  M  :  n:\mBbbN{}  {}\mrightarrow{}  (i:\mBbbN{}n  {}\mrightarrow{}  (B  i))  {}\mrightarrow{}  (T?)
7.  [\%5]  :  \mforall{}f:i:\mBbbN{}  {}\mrightarrow{}  (B  i)
                        ((\mexists{}n:\mBbbN{}.  ((M  n  f)  =  (inl  (F  f))))  \mwedge{}  (\mforall{}n:\mBbbN{}.  (M  n  f)  =  (inl  (F  f))  supposing  \muparrow{}isl(M  n  f)))
8.  \mexists{}k:\mBbbN{}  [(\mforall{}f:i:\mBbbN{}  {}\mrightarrow{}  (B  i).  \mexists{}n:\mBbbN{}k.  (\muparrow{}isl(M  n  f)))]
\mvdash{}  \mexists{}n:\mBbbN{}.  \mforall{}f,g:i:\mBbbN{}  {}\mrightarrow{}  (B  i).    ((f  =  g)  {}\mRightarrow{}  ((F  f)  =  (F  g)))


By

---

Latex:
ExRepD

---

Home Index