---

Step * of Lemma qv-convex-all

∀[T:Type]. ∀[S:T ⟶ (ℚ List) ⟶ ℙ].  ((∀x:T. qv-convex(p.S[x;p])) ⇒ qv-convex(p.∀x:T. S[x;p]))
BY
{ (Auto THEN All (Unfold `qv-convex`) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[S:T  {}\mrightarrow{}  (\mBbbQ{}  List)  {}\mrightarrow{}  \mBbbP{}].    ((\mforall{}x:T.  qv-convex(p.S[x;p]))  {}\mRightarrow{}  qv-convex(p.\mforall{}x:T.  S[x;p]))


By

---

Latex:
(Auto  THEN  All  (Unfold  `qv-convex`)  THEN  Auto)

---

Home Index