some edits

FEM/quadrature.v

@@ -32,8 +32,8 @@ Variable d : nat. (* d = dimension de l'espace de départ E C R^d *)
 Variable P : (E -> R) -> Prop. (* ss ens de l'ensemble de fcts E -> R*)
 Variable Nk : nat. (* Nk = dimension de l'espace de polynôme Pk(T) de triangle *)
 Variable vert : nat -> E. (* vertices = les sommets de l'élt géom = suite *)
-Variable Nb_vert : nat. (* le nombre de sommets dans tout E *)
-Hypothesis H_vert : (d < Nb_vert)%nat. (* dim E < Nb of vertices*)
+Variable Card_sigma : nat. (*Nb_vert*) (* le nombre de sommets dans tout E *)
+Hypothesis Hyp_vert : (d < Card_sigma)%nat. (* dim E < cardinal of Sigma *)
 
 (* modéliser l'ev des fonctions à valeurs dans un ev pour abstraire (pour le rendre général) l'espace des polynomes ?? *)
 
@@ -45,41 +45,45 @@ Check (Pol (fun _ => 0)).
 Check (dim Pol).
 (* fin essai *)
 
-
 Definition geom : E -> Prop := 
   fun x => exists a : nat -> R, 
-  (x = sum_n (fun i => scal (a i) (vert i)) Nb_vert) /\ 
-  (forall i, (i < Nb_vert)%nat -> 0 <= a i <= 1).
+  (x = sum_n (fun i => scal (a i) (vert i)) Card_sigma) /\ 
+  (forall i, (i < Card_sigma)%nat -> 0 <= a i <= 1).
 (* hypothèses sur vert : forme géometrique non dégénerée *)
 
 Variable sigma : nat -> (E -> R) -> R.  (* après definir P: nat -> P -> R *)
-Hypothesis H_sigma_1 : forall i, (i < Nb_vert)%nat -> is_linear_mapping (sigma i).
+Hypothesis H_sigma_1 : forall i, (i < Card_sigma)%nat -> is_linear_mapping (sigma i).
 Definition sigma_hyp :=
  fun p => (* hyp que p est poly de deg <= k *)
-  (forall i, (i < Nb_vert)%nat ->  sigma i p = 0) -> forall x, p x = 0.
+  (forall i, (i < Card_sigma)%nat ->  sigma i p = 0) -> forall x, p x = 0.
 (* p sera le polynôme nul + faut des hypthèses sur les polynômes *) 
 
-(* lemme: Sigma={sigma(i) pour i < Nk} est une bijection entre Pk et R^Nk  -> conséquence de H_sigma_2 *)
+(* lemme: Sigma={sigma(i) pour i < Card_sigma} est une bijection entre Pk et R^Card_sigma -> conséquence de H_sigma_2 *)
 
 (* next step : poly de ssreflect mathcomp analysis et en dim qcq ?*)
 
 Hypothesis H_sigma_2 : forall p (* hyp que p est poly de deg <= k *), 
-  (forall i, (i < Nb_vert)%nat ->  sigma i p = 0) -> forall x, p x = 0.
+  (forall i, (i < Card_sigma)%nat ->  sigma i p = 0) -> forall x, p x = 0.
 
 Definition is_unisolvant : Prop :=  (*forall f : P,*)
-  forall a : nat -> R, exists! f, Pol f /\ (forall i, (i < Nb_vert)%nat -> sigma i f = a i).
+  forall a : nat -> R, exists! f, Pol f /\ (forall i, (i < Card_sigma)%nat -> sigma i f = a i).
 
 Lemma is_unisolvant_equiv : 
    is_unisolvant <->
-   (Nk = Nb_vert) /\
-   (exists p,(forall i, (i < Nb_vert)%nat -> sigma i p = 0) -> forall x, p x = 0).
+   (Nk = Card_sigma) /\
+   (exists p,(forall i, (i < Card_sigma)%nat -> sigma i p = 0) -> forall x, p x = 0).
+Proof.
+split; intros H1.
+unfold is_unisolvant in H1.
+split.
+
 Admitted.
 
 (** \poly_(i < n) E i   is the polynomial:
     (E 0) + (E 1)  *: 'X + ...  + E (n - 1) *: 'X^(n-1) *)
 
-(*Variable Pk : E -> R !!*)
-Let Pk: {poly R}:= \poly_(i < S k ) i%:R.
+(*Variable Pk : E -> R !!
+Let Pk: {poly R}:= \poly_(i < S k ) i%:R.*)
 
 End Finite_EM.