---

Step * of Lemma uniform-continuity-from-fan3

∀[T:Type]
  ((∃P:ℕ ⟶ ℙ. ∃a:ℕ. (P[a] ∧ (∀n:ℕ. Dec(P[n])) ∧ (∃h:T ⟶ {n:ℕ| P[n]} . Bij(T;{n:ℕ| P[n]} ;h))))
  ⇒ (∀F:(ℕ ⟶ 𝔹) ⟶ T. ⇃(∃n:ℕ. ∀f,g:ℕ ⟶ 𝔹.  ((f = g ∈ (ℕn ⟶ 𝔹)) ⇒ ((F f) = (F g) ∈ T)))))
BY
{ (InstLemma `uniform-continuity-from-fan2` [] ⋅
   THEN (ParallelLast' THEN Auto)
   THEN D 2
   THEN Auto
   THEN ExRepD
   THEN D 0 With ⌜{n:ℕ| P[n]} ⌝ 
   THEN Auto) }

1
1. [T] : Type
2. P : ℕ ⟶ ℙ@i'
3. a : ℕ@i'
4. P[a]
5. ∀n:ℕ. Dec(P[n])
6. h : T ⟶ {n:ℕ| P[n]} @i'
7. Bij(T;{n:ℕ| P[n]} ;h)
8. F : (ℕ ⟶ 𝔹) ⟶ T@i
9. {n:ℕ| P[n]}  ⊆r ℕ
⊢ ∃r:ℕ ⟶ {n:ℕ| P[n]} . ∀x:{n:ℕ| P[n]} . ((r x) = x ∈ {n:ℕ| P[n]} )

---

Latex:

---

Latex:
\mforall{}[T:Type]
    ((\mexists{}P:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}.  \mexists{}a:\mBbbN{}.  (P[a]  \mwedge{}  (\mforall{}n:\mBbbN{}.  Dec(P[n]))  \mwedge{}  (\mexists{}h:T  {}\mrightarrow{}  \{n:\mBbbN{}|  P[n]\}  .  Bij(T;\{n:\mBbbN{}|  P[n]\}  ;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:
(InstLemma  `uniform-continuity-from-fan2`  []  \mcdot{}
  THEN  (ParallelLast'  THEN  Auto)
  THEN  D  2
  THEN  Auto
  THEN  ExRepD
  THEN  D  0  With  \mkleeneopen{}\{n:\mBbbN{}|  P[n]\}  \mkleeneclose{} 
  THEN  Auto)

---

Home Index