---

Step * of Lemma uniform-continuity-from-fan-ext

∀[T:Type]
  ∀F:(ℕ ⟶ 𝔹) ⟶ T
    (⇃(∃M:n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ (T?) [(∀f:ℕ ⟶ 𝔹
                                       ((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (T?)))
                                       ∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (T?) supposing ↑isl(M n f))))])
    ⇒ ⇃(∃n:ℕ. ∀f,g:ℕ ⟶ 𝔹.  ((f = g ∈ (ℕn ⟶ 𝔹)) ⇒ ((F f) = (F g) ∈ T))))
BY
{ Extract of Obid: uniform-continuity-from-fan
  not unfolding  bottom bar_recursion FAN int_seg_decide outl
  finishing with (RepUR ``btrue bfalse it ucont`` 0 THEN Auto)
  normalizes to:
  
  λF,M. ucont(F;M) }

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}F:(\mBbbN{}  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  T
        (\00D9(\mexists{}M:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  (T?)  [(\mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}
                                                                              ((\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))))])
        {}\mRightarrow{}  \00D9(\mexists{}n:\mBbbN{}.  \mforall{}f,g:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.    ((f  =  g)  {}\mRightarrow{}  ((F  f)  =  (F  g)))))


By

---

Latex:
Extract  of  Obid:  uniform-continuity-from-fan
not  unfolding    bottom  bar\_recursion  FAN  int\_seg\_decide  outl
finishing  with  (RepUR  ``btrue  bfalse  it  ucont``  0  THEN  Auto)
normalizes  to:

\mlambda{}F,M.  ucont(F;M)

---

Home Index