---

Step * of Lemma weak-continuity-nat-int-bool

∀F:(ℕ ⟶ ℤ) ⟶ 𝔹. ∀f:ℕ ⟶ ℤ.  ⇃(∃n:ℕ. ∀g:ℕ ⟶ ℤ. ((f = g ∈ (ℕn ⟶ ℤ)) ⇒ F f = F g))
BY
{ (InstLemma `weak-continuity-nat-int` []⋅
   THEN Auto
   THEN (InstHyp [⌜λf.if F f then 1 else 0 fi ⌝;⌜f⌝] 1⋅ THENA Auto)
   THEN Reduce -1
   THEN RepeatFor 4 ((ParallelLast THENA Auto))) }

1
1. ∀F:(ℕ ⟶ ℤ) ⟶ ℕ. ∀f:ℕ ⟶ ℤ.  ⇃(∃n:ℕ. ∀g:ℕ ⟶ ℤ. ((f = g ∈ (ℕn ⟶ ℤ)) ⇒ ((F f) = (F g) ∈ ℕ)))
2. F : (ℕ ⟶ ℤ) ⟶ 𝔹
3. f : ℕ ⟶ ℤ
4. n : ℕ
5. ∀g:ℕ ⟶ ℤ. ((f = g ∈ (ℕn ⟶ ℤ)) ⇒ (if F f then 1 else 0 fi  = if F g then 1 else 0 fi  ∈ ℕ))
6. g : ℕ ⟶ ℤ
7. f = g ∈ (ℕn ⟶ ℤ)
8. if F f then 1 else 0 fi  = if F g then 1 else 0 fi  ∈ ℕ
⊢ F f = F g

---

Latex:

---

Latex:
\mforall{}F:(\mBbbN{}  {}\mrightarrow{}  \mBbbZ{})  {}\mrightarrow{}  \mBbbB{}.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbZ{}.    \00D9(\mexists{}n:\mBbbN{}.  \mforall{}g:\mBbbN{}  {}\mrightarrow{}  \mBbbZ{}.  ((f  =  g)  {}\mRightarrow{}  F  f  =  F  g))


By

---

Latex:
(InstLemma  `weak-continuity-nat-int`  []\mcdot{}
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}\mlambda{}f.if  F  f  then  1  else  0  fi  \mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]  1\mcdot{}  THENA  Auto)
  THEN  Reduce  -1
  THEN  RepeatFor  4  ((ParallelLast  THENA  Auto)))

---

Home Index