---

Step * of Lemma decidable__all_int_seg

∀i,j:ℤ.  ∀[F:{i..j-} ⟶ ℙ{u}]. ((∀k:{i..j-}. Dec(F[k])) ⇒ Dec(∀k:{i..j-}. F[k]))
BY
{ (Auto THEN All (Unfold `so_apply`) THEN (InstLemma `decidable__exists_int_seg` [⌜i⌝;⌜j⌝;⌜λ2x.¬(F x)⌝]⋅ THENA Auto)) }

1
1. i : ℤ@i
2. j : ℤ@i
3. [F] : {i..j-} ⟶ ℙ{u}
4. ∀k:{i..j-}. Dec(F k)@[u | i]
5. Dec(∃k:{i..j-}. (¬(F k)))
⊢ Dec(∀k:{i..j-}. (F k))

---

Latex:

---

Latex:
\mforall{}i,j:\mBbbZ{}.    \mforall{}[F:\{i..j\msupminus{}\}  {}\mrightarrow{}  \mBbbP{}\{u\}].  ((\mforall{}k:\{i..j\msupminus{}\}.  Dec(F[k]))  {}\mRightarrow{}  Dec(\mforall{}k:\{i..j\msupminus{}\}.  F[k]))


By

---

Latex:
(Auto
  THEN  All  (Unfold  `so\_apply`)
  THEN  (InstLemma  `decidable\_\_exists\_int\_seg`  [\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.\mneg{}(F  x)\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index