---

Step * of Lemma uniform-continuity-from-fan2

∀[T:Type]
  ((∃U:Type. ((U ⊆r ℕ) ∧ (∃r:ℕ ⟶ U. ∀x:U. ((r x) = x ∈ U)) ∧ (∃h:T ⟶ U. Bij(T;U;h))))
  ⇒ (∀F:(ℕ ⟶ 𝔹) ⟶ T. ⇃(∃n:ℕ. ∀f,g:ℕ ⟶ 𝔹.  ((f = g ∈ (ℕn ⟶ 𝔹)) ⇒ ((F f) = (F g) ∈ T)))))
BY
{ (Auto
   THEN BLemma `uniform-continuity-from-fan`
   THEN Auto
   THEN ExRepD
   THEN InstLemma `strong-continuity2-half-squash-surject-biject`
    [⌜𝔹⌝;⌜T⌝;⌜U⌝;⌜F⌝]⋅
   THEN Auto
   THEN RepeatFor 2 ((ParallelLast THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[T:Type]
    ((\mexists{}U:Type.  ((U  \msubseteq{}r  \mBbbN{})  \mwedge{}  (\mexists{}r:\mBbbN{}  {}\mrightarrow{}  U.  \mforall{}x:U.  ((r  x)  =  x))  \mwedge{}  (\mexists{}h:T  {}\mrightarrow{}  U.  Bij(T;U;h))))
    {}\mRightarrow{}  (\mforall{}F:(\mBbbN{}  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  T.  \00D9(\mexists{}n:\mBbbN{}.  \mforall{}f,g:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.    ((f  =  g)  {}\mRightarrow{}  ((F  f)  =  (F  g))))))


By

---

Latex:
(Auto
  THEN  BLemma  `uniform-continuity-from-fan`
  THEN  Auto
  THEN  ExRepD
  THEN  InstLemma  `strong-continuity2-half-squash-surject-biject`
    [\mkleeneopen{}\mBbbB{}\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}U\mkleeneclose{};\mkleeneopen{}F\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  RepeatFor  2  ((ParallelLast  THEN  Auto)))

---

Home Index