---

Step * of Lemma decidable-exists-iseg

∀[T:Type]. ∀[P:(T List) ⟶ ℙ].  ((∀L:T List. Dec(P[L])) ⇒ (∀L:T List. Dec(∃L':T List. (L' ≤ L ∧ P[L']))))
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:(T  List)  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}L:T  List.  Dec(P[L]))  {}\mRightarrow{}  (\mforall{}L:T  List.  Dec(\mexists{}L':T  List.  (L'  \mleq{}  L  \mwedge{}  P[L']))))


By

---

Latex:
Auto

---

Home Index