---

Step * of Lemma uniform-continuity-from-fan

∀[T:Type]
  ∀F:(ℕ ⟶ 𝔹) ⟶ T
    (⇃(∃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))))])
    ⇒ ⇃(∃n:ℕ. ∀f,g:ℕ ⟶ 𝔹.  ((f = g ∈ (ℕn ⟶ 𝔹)) ⇒ ((F f) = (F g) ∈ T))))
BY
{ (Auto
   THEN (UnHalfSquash THENA Auto)
   THEN (UnHalfSquashConcl THENA Auto)
   THEN D -1
   THEN (InstLemma `fan_theorem-ext` [⌜λn,f. (↑isl(M n f))⌝]⋅ THENA Auto)
   THEN All(RepUR ``so_apply``)) }

1
1. T : Type
2. F : (ℕ ⟶ 𝔹) ⟶ T
3. M : n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ (T?)
4. ∀f:ℕ ⟶ 𝔹. ((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (T?))) ∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (T?) supposing ↑isl(M n f)))
5. f : ℕ ⟶ 𝔹
⊢ ↓∃n:ℕ. (↑isl(M n f))

2
1. [T] : Type
2. F : (ℕ ⟶ 𝔹) ⟶ T
3. M : n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ (T?)
4. [%2] : ∀f:ℕ ⟶ 𝔹
            ((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (T?))) ∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (T?) supposing ↑isl(M n f)))
5. n : ℕ
6. s : ℕn ⟶ 𝔹
⊢ Dec(↑isl(M n s))

3
1. [T] : Type
2. F : (ℕ ⟶ 𝔹) ⟶ T
3. M : n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ (T?)
4. [%2] : ∀f:ℕ ⟶ 𝔹
            ((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (T?))) ∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (T?) supposing ↑isl(M n f)))
5. ∃k:ℕ. ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. (↑isl(M n f))
⊢ ∃n:ℕ. ∀f,g:ℕ ⟶ 𝔹.  ((f = g ∈ (ℕn ⟶ 𝔹)) ⇒ ((F f) = (F g) ∈ T))

---

Latex:

---

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


By

---

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

---

Home Index