---

Step * 3 of Lemma general-cantor-to-int-uniform-continuity-half-squashed


1. B : ℕ ⟶ ℕ+
2. F : (i:ℕ ⟶ ℕB[i]) ⟶ ℤ
⊢ ⇃(∃M:n:ℕ ⟶ (i:ℕn ⟶ ℕB[i]) ⟶ (ℤ?) [(∀f:i:ℕ ⟶ ℕB[i]
                                          ((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (ℤ?)))
                                          ∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (ℤ?) supposing ↑isl(M n f))))])
BY
{ (InstLemma `strong-continuity2-half-squash-surject-biject-ext` [⌜i:ℕ × ℕB[i]⌝;⌜ℤ⌝;⌜ℕ⌝]⋅ THENA Auto) }

1
.....antecedent..... 
1. B : ℕ ⟶ ℕ+
2. F : (i:ℕ ⟶ ℕB[i]) ⟶ ℤ
⊢ ∃r:ℕ ⟶ ℕ. ∀x:ℕ. ((r x) = x ∈ ℕ)

2
1. B : ℕ ⟶ ℕ+
2. F : (i:ℕ ⟶ ℕB[i]) ⟶ ℤ
3. ∀F:(ℕ ⟶ (i:ℕ × ℕB[i])) ⟶ ℤ
     ⇃(∃M:n:ℕ ⟶ (ℕn ⟶ (i:ℕ × ℕB[i])) ⟶ (ℤ?)
        ∀f:ℕ ⟶ (i:ℕ × ℕB[i])
          ((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (ℤ?))) ∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (ℤ?) supposing ↑isl(M n f))))
⊢ ⇃(∃M:n:ℕ ⟶ (i:ℕn ⟶ ℕB[i]) ⟶ (ℤ?) [(∀f:i:ℕ ⟶ ℕB[i]
                                          ((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (ℤ?)))
                                          ∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (ℤ?) supposing ↑isl(M n f))))])

---

Latex:

---

Latex:

1.  B  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}\msupplus{}
2.  F  :  (i:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[i])  {}\mrightarrow{}  \mBbbZ{}
\mvdash{}  \00D9(\mexists{}M:n:\mBbbN{}  {}\mrightarrow{}  (i:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}B[i])  {}\mrightarrow{}  (\mBbbZ{}?)  [(\mforall{}f:i:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}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))))])


By

---

Latex:
(InstLemma  `strong-continuity2-half-squash-surject-biject-ext`  [\mkleeneopen{}i:\mBbbN{}  \mtimes{}  \mBbbN{}B[i]\mkleeneclose{};\mkleeneopen{}\mBbbZ{}\mkleeneclose{};\mkleeneopen{}\mBbbN{}\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index