---

Step * of Lemma ucont_wf

∀[T:Type]. ∀[F:(ℕ ⟶ 𝔹) ⟶ T]. ∀[M:⇃(∃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))))])].
  (ucont(F;M) ∈ ⇃(∃n:ℕ. ∀f,g:ℕ ⟶ 𝔹.  ((f = g ∈ (ℕn ⟶ 𝔹)) ⇒ ((F f) = (F g) ∈ T))))
BY
{ (Auto
   THEN (Subst' ucont(F;M) ~ TERMOF{uniform-continuity-from-fan-ext:o, \\v:l, i:l} F M 0 THENA (Computation THEN Auto))
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (Subst'  ucont(F;M)  \msim{}  TERMOF\{uniform-continuity-from-fan-ext:o,  \mbackslash{}\mbackslash{}v:l,  i:l\}  F  M  0
              THENA  (Computation  THEN  Auto)
              )
  THEN  Auto)

---

Home Index