---

Step * of Lemma int-seg-case-monotone

∀[i,j:ℤ]. ∀[F,G:{i..j-} ⟶ ℙ]. ∀[d:∀k:{i..j-}. (F[k] ∨ G[k])].
  ∀k:{i..j + 1-}. ((↑isl(int-seg-case(i;k;d))) ⇒ (∀k':{k..j + 1-}. (↑isl(int-seg-case(i;k';d)))))
BY
{ Auto }

1
1. i : ℤ
2. j : ℤ
3. F : {i..j-} ⟶ ℙ
4. G : {i..j-} ⟶ ℙ
5. d : ∀k:{i..j-}. (F[k] ∨ G[k])
6. k : {i..j + 1-}
7. ↑isl(int-seg-case(i;k;d))
8. k' : {k..j + 1-}
⊢ ↑isl(int-seg-case(i;k';d))

---

Latex:

---

Latex:
\mforall{}[i,j:\mBbbZ{}].  \mforall{}[F,G:\{i..j\msupminus{}\}  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[d:\mforall{}k:\{i..j\msupminus{}\}.  (F[k]  \mvee{}  G[k])].
    \mforall{}k:\{i..j  +  1\msupminus{}\}.  ((\muparrow{}isl(int-seg-case(i;k;d)))  {}\mRightarrow{}  (\mforall{}k':\{k..j  +  1\msupminus{}\}.  (\muparrow{}isl(int-seg-case(i;k';d)))))


By

---

Latex:
Auto

---

Home Index