---

Step * of Lemma geo-convex-intersection

∀[g:BasicGeometry]. ∀[T:Type].  ∀P:T ⟶ Point ⟶ ℙ. ((∀t:T. IsConvex(x.P[t;x])) ⇒ IsConvex(x.∀t:T. P[t;x]))
BY
{ (Unfold `geo-convex` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[g:BasicGeometry].  \mforall{}[T:Type].
    \mforall{}P:T  {}\mrightarrow{}  Point  {}\mrightarrow{}  \mBbbP{}.  ((\mforall{}t:T.  IsConvex(x.P[t;x]))  {}\mRightarrow{}  IsConvex(x.\mforall{}t:T.  P[t;x]))


By

---

Latex:
(Unfold  `geo-convex`  0  THEN  Auto)

---

Home Index