---

Step * of Lemma l_all_exists_max

∀[A:Type]. ∀[R:A ⟶ ℤ ⟶ ℙ].
  ((∀x:A. ∀n,m:ℤ.  (R[x;n] ⇒ R[x;m] supposing n ≤ m)) ⇒ (∀L:A List. ((∀x∈L.∃n:ℤ. R[x;n]) ⇒ (∃n:ℤ. (∀x∈L.R[x;n])))))
BY
{ InductionOnList }

1
1. [A] : Type
2. [R] : A ⟶ ℤ ⟶ ℙ
3. ∀x:A. ∀n,m:ℤ.  (R[x;n] ⇒ R[x;m] supposing n ≤ m)@i
⊢ (∀x∈[].∃n:ℤ. R[x;n]) ⇒ (∃n:ℤ. (∀x∈[].R[x;n]))

2
1. [A] : Type
2. [R] : A ⟶ ℤ ⟶ ℙ
3. ∀x:A. ∀n,m:ℤ.  (R[x;n] ⇒ R[x;m] supposing n ≤ m)@i
4. u : A@i
5. v : A List@i
6. (∀x∈v.∃n:ℤ. R[x;n]) ⇒ (∃n:ℤ. (∀x∈v.R[x;n]))@i
⊢ (∀x∈[u / v].∃n:ℤ. R[x;n]) ⇒ (∃n:ℤ. (∀x∈[u / v].R[x;n]))

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[R:A  {}\mrightarrow{}  \mBbbZ{}  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}x:A.  \mforall{}n,m:\mBbbZ{}.    (R[x;n]  {}\mRightarrow{}  R[x;m]  supposing  n  \mleq{}  m))
    {}\mRightarrow{}  (\mforall{}L:A  List.  ((\mforall{}x\mmember{}L.\mexists{}n:\mBbbZ{}.  R[x;n])  {}\mRightarrow{}  (\mexists{}n:\mBbbZ{}.  (\mforall{}x\mmember{}L.R[x;n])))))


By

---

Latex:
InductionOnList

---

Home Index