The Coq mailing list

["Nickolay V. Shmyrev" <nshmyrev AT yandex.ru>]

Hello all.

I am trying to play with CoQ a bit. I've written the following theorem
about convexity but have no idea how to prove it. Either I don't
understand something or it's really non-trivial thing. Please help. 

Thanks a lot.

------------------------------------------------------------------

Require Import Linear_Algebra_by_Friedberg_Insel_Spence.

Variable F : field.
Variable V : vectorspace F.

Definition min_set (X : part_set V) : part_set V.
intros.
simpl in |- *.
apply
 Build_Predicate
  with
    (fun x : V =>
     exists s : X, x =' (min subtype_elt s) in _).
red in |- *.
intros.
inversion_clear H.
exists x0.
apply Trans with x; auto with algebra.
Defined.

Definition is_convex (X : part_set V) :=
    forall s1 s2 : X, (exists s3 : X, subtype_elt s3 +' subtype_elt s3 =' 
subtype_elt s1 +' subtype_elt s2 in _).


Lemma min_is_convex :
    forall X : part_set V, is_convex X -> is_convex (min_set X).