alternative definition of convexity

[affeldt-aist]

analysis/theories/normedtype_theory/tvs.v

Lines 309 to 311 in 0a1e66d

	Definition convex (R : numDomainType) (M : lmodType R) (A : set M) :=
	forall x y (lambda : R), x \in A -> y \in A ->
	0 < lambda -> lambda < 1 -> lambda *: x + (1 - lambda) *: y \in A.

This definition ought to be in convex.v.

@mkerjean

[affeldt-aist]

This has been fixed by PR #1887, now merged.