---

Step * of Lemma decidable-exists-int_seg-subtype

∀[i:ℤ]. ∀[j:{i + 1...}]. ∀[P:{i..j-} ⟶ ℙ].  Dec(∃k:{i + 1..j-}. P[k]) ⊆r Dec(∃k:{i..j-}. P[k]) supposing ¬P[i]
BY
{ (Auto THEN BLemma `decidable-subtype` THEN Auto THEN ParallelLast THEN Auto) }

1
1. i : ℤ
2. j : {i + 1...}
3. P : {i..j-} ⟶ ℙ
4. ¬P[i]
5. k : ℤ@i
6. i ≤ k@i
7. k < j@i
8. P[k]@i
⊢ (i + 1) ≤ k

---

Latex:

---

Latex:
\mforall{}[i:\mBbbZ{}].  \mforall{}[j:\{i  +  1...\}].  \mforall{}[P:\{i..j\msupminus{}\}  {}\mrightarrow{}  \mBbbP{}].
    Dec(\mexists{}k:\{i  +  1..j\msupminus{}\}.  P[k])  \msubseteq{}r  Dec(\mexists{}k:\{i..j\msupminus{}\}.  P[k])  supposing  \mneg{}P[i]


By

---

Latex:
(Auto  THEN  BLemma  `decidable-subtype`  THEN  Auto  THEN  ParallelLast  THEN  Auto)

---

Home Index