Step * of Lemma ucont_wf

[T:Type]. ∀[F:(ℕ ⟶ 𝔹) ⟶ T]. ∀[M:⇃(∃M:n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ (T?) [(∀f:ℕ ⟶ 𝔹
                                                                     ((∃n:ℕ((M f) (inl (F f)) ∈ (T?)))
                                                                     ∧ (∀n:ℕ
                                                                          (M f) (inl (F f)) ∈ (T?) 
                                                                          supposing ↑isl(M 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} 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