---

Step * of Lemma int_seg_decide_wf

∀[i,j:ℤ]. ∀[F:{i..j-} ⟶ ℙ{u}]. ∀[d:∀k:{i..j-}. Dec(F[k])].  (int_seg_decide(d;i;j) ∈ Dec(∃k:{i..j-}. F[k]))
BY
{ TACTIC:Auto }

1
1. i : ℤ
2. j : ℤ
3. F : {i..j-} ⟶ ℙ{u}
4. d : ∀k:{i..j-}. Dec(F[k])
⊢ int_seg_decide(d;i;j) ∈ Dec(∃k:{i..j-}. F[k])

---

Latex:

---

Latex:
\mforall{}[i,j:\mBbbZ{}].  \mforall{}[F:\{i..j\msupminus{}\}  {}\mrightarrow{}  \mBbbP{}\{u\}].  \mforall{}[d:\mforall{}k:\{i..j\msupminus{}\}.  Dec(F[k])].
    (int\_seg\_decide(d;i;j)  \mmember{}  Dec(\mexists{}k:\{i..j\msupminus{}\}.  F[k]))


By

---

Latex:
TACTIC:Auto

---

Home Index