Skip to content
Snippets Groups Projects
Commit 1742703e authored by Mouhcine's avatar Mouhcine
Browse files

FE compiles

parent 5c3b77ad
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 0 additions and 3 deletions
FEM/finite_element.v
+ 0
− 3
View file @ 1742703e
......@@ -425,9 +425,6 @@ Definition T_geom_inv : 'R^dd -> 'R^dd := fun x =>
Variable PE PF : 'R^dd -> Prop.
Lemma T_geom_inv_is_bij_id :
is_bij_id P_approx_ref P_approx_ref T_geom T_geom_inv.
(* Dans FD y'a pas le lemme de bij <-> inj /\ surj ? *)
Lemma T_geom_inv_correct1 : forall x : 'R^dd,
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment