---

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

No Annotations
∀[B:ℕ ⟶ Type]
  ⇃(∀i:ℕ. ∀K:B[i] ⟶ ℕ.  (∃Bnd:ℕ [(∀t:B[i]. ((K t) ≤ Bnd))]))
  ⇒ (∀[T:Type]
        ∀F:(i:ℕ ⟶ B[i]) ⟶ T
          (⇃(∃M:n:ℕ ⟶ (i:ℕn ⟶ B[i]) ⟶ (T?) [(∀f:i:ℕ ⟶ B[i]
                                                  ((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (T?)))
                                                  ∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (T?) supposing ↑isl(M n f))))])
          ⇒ ⇃(∃n:ℕ. ∀f,g:i:ℕ ⟶ B[i].  ((f = g ∈ (i:ℕn ⟶ B[i])) ⇒ ((F f) = (F g) ∈ T))))) 
  supposing ∀i:ℕ. B[i]
BY
{ (Intros
   THEN (UnHalfSquash THENA Auto)
   THEN (UnHalfSquashConcl THENA Auto)
   THEN D -1
   THEN (InstLemma `simple_more_general_fan_theorem-ext` [⌜B⌝;⌜λn,f. (↑isl(M n f))⌝]⋅ THENA Auto)
   THEN All(RepUR ``so_apply``)) }

1
1. [B] : ℕ ⟶ Type
2. [%] : ∀i:ℕ. (B i)
3. ∀i:ℕ. ∀K:(B i) ⟶ ℕ.  (∃Bnd:ℕ [(∀t:B i. ((K t) ≤ Bnd))])
4. [T] : Type
5. F : (i:ℕ ⟶ (B i)) ⟶ T
6. M : n:ℕ ⟶ (i:ℕn ⟶ (B i)) ⟶ (T?)
7. [%5] : ∀f:i:ℕ ⟶ (B i)
            ((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (T?))) ∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (T?) supposing ↑isl(M n f)))
8. i : ℕ
⊢ Bounded(B i)

2
1. B : ℕ ⟶ Type
2. ∀i:ℕ. (B i)
3. ∀i:ℕ. ∀K:(B i) ⟶ ℕ.  (∃Bnd:ℕ [(∀t:B i. ((K t) ≤ Bnd))])
4. T : Type
5. F : (i:ℕ ⟶ (B i)) ⟶ T
6. M : n:ℕ ⟶ (i:ℕn ⟶ (B i)) ⟶ (T?)
7. ∀f:i:ℕ ⟶ (B i)
     ((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (T?))) ∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (T?) supposing ↑isl(M n f)))
8. f : i:ℕ ⟶ (B i)
⊢ ↓∃n:ℕ. (↑isl(M n f))

3
1. [B] : ℕ ⟶ Type
2. [%] : ∀i:ℕ. (B i)
3. ∀i:ℕ. ∀K:(B i) ⟶ ℕ.  (∃Bnd:ℕ [(∀t:B i. ((K t) ≤ Bnd))])
4. [T] : Type
5. F : (i:ℕ ⟶ (B i)) ⟶ T
6. M : n:ℕ ⟶ (i:ℕn ⟶ (B i)) ⟶ (T?)
7. [%5] : ∀f:i:ℕ ⟶ (B i)
            ((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (T?))) ∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (T?) supposing ↑isl(M n f)))
8. n : ℕ
9. s : i:ℕn ⟶ (B i)
⊢ Dec(↑isl(M n s))

4
1. [B] : ℕ ⟶ Type
2. [%] : ∀i:ℕ. (B i)
3. ∀i:ℕ. ∀K:(B i) ⟶ ℕ.  (∃Bnd:ℕ [(∀t:B i. ((K t) ≤ Bnd))])
4. [T] : Type
5. F : (i:ℕ ⟶ (B i)) ⟶ T
6. M : n:ℕ ⟶ (i:ℕn ⟶ (B i)) ⟶ (T?)
7. [%5] : ∀f:i:ℕ ⟶ (B i)
            ((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (T?))) ∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (T?) supposing ↑isl(M n f)))
8. ∃k:ℕ [(∀f:i:ℕ ⟶ (B i). ∃n:ℕk. (↑isl(M n f)))]
⊢ ∃n:ℕ. ∀f,g:i:ℕ ⟶ (B i).  ((f = g ∈ (i:ℕn ⟶ (B i))) ⇒ ((F f) = (F g) ∈ T))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[B:\mBbbN{}  {}\mrightarrow{}  Type]
    \00D9(\mforall{}i:\mBbbN{}.  \mforall{}K:B[i]  {}\mrightarrow{}  \mBbbN{}.    (\mexists{}Bnd:\mBbbN{}  [(\mforall{}t:B[i].  ((K  t)  \mleq{}  Bnd))]))
    {}\mRightarrow{}  (\mforall{}[T:Type]
                \mforall{}F:(i:\mBbbN{}  {}\mrightarrow{}  B[i])  {}\mrightarrow{}  T
                    (\00D9(\mexists{}M:n:\mBbbN{}  {}\mrightarrow{}  (i:\mBbbN{}n  {}\mrightarrow{}  B[i])  {}\mrightarrow{}  (T?)  [(\mforall{}f:i:\mBbbN{}  {}\mrightarrow{}  B[i]
                                                                                                    ((\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:i:\mBbbN{}  {}\mrightarrow{}  B[i].    ((f  =  g)  {}\mRightarrow{}  ((F  f)  =  (F  g)))))) 
    supposing  \mforall{}i:\mBbbN{}.  B[i]


By

---

Latex:
(Intros
  THEN  (UnHalfSquash  THENA  Auto)
  THEN  (UnHalfSquashConcl  THENA  Auto)
  THEN  D  -1
  THEN  (InstLemma  `simple\_more\_general\_fan\_theorem-ext`  [\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}\mlambda{}n,f.  (\muparrow{}isl(M  n  f))\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  All(RepUR  ``so\_apply``))

---

Home Index