From 917f998ccaabfa98296772d74e7d8a13b38aab25 Mon Sep 17 00:00:00 2001
From: Pierre Rousselin <rousselin@math.univ-paris13.fr>
Date: Sun, 20 Nov 2022 19:40:37 +0100
Subject: [PATCH] cght mineur
---
FEM/Finite_dim.v | 2 +-
FEM/comb_lin.v | 7 +++----
2 files changed, 4 insertions(+), 5 deletions(-)
diff --git a/FEM/Finite_dim.v b/FEM/Finite_dim.v
index 290e508a..101651ff 100644
--- a/FEM/Finite_dim.v
+++ b/FEM/Finite_dim.v
@@ -206,7 +206,7 @@ Proof.
remember (fun i => proj1_sig (Gi_Li i)) as M eqn:defM.
exists (fun j => (comb_lin Lx (fun i => M i j))).
rewrite <-comb_lin_switch.
- f_equal; apply functional_extensionality; intros i.
+ f_equal; extensionality i.
rewrite defM; simpl.
apply (proj2_sig (Gi_Li i)).
- intros [L]; apply (has_generator_is_comb_lin_stable _ G); assumption.
diff --git a/FEM/comb_lin.v b/FEM/comb_lin.v
index 9f9d8ca9..859d33cd 100644
--- a/FEM/comb_lin.v
+++ b/FEM/comb_lin.v
@@ -116,8 +116,7 @@ Proof.
rewrite <-scal_opp_one.
rewrite comb_lin_scal.
apply comb_lin_ext_l.
- apply sym_eq, functional_extensionality.
- intros i; apply scal_opp_one.
+ apply sym_eq; extensionality i; apply scal_opp_one.
Qed.
Lemma comb_lin_nil (L : 'R^0) (B : 'E^0) :
@@ -229,14 +228,14 @@ Proof.
assert (fplus : (fun i : [0..n[ => f i (plus x y))
= plus (fun i => f i x) (fun i => f i y)). {
unfold plus at 2; simpl; unfold fct_plus.
- apply functional_extensionality; intros i; apply H.
+ extensionality i; apply H.
}
now rewrite fplus; rewrite comb_lin_plus_l.
- intros x l.
assert (fscal : (fun i : [0..n[ => f i (scal l x))
= scal l (fun i => f i x)). {
unfold scal at 2; simpl; unfold fct_scal.
- apply functional_extensionality; intros i; apply H.
+ extensionality i; apply H.
}
now rewrite fscal; rewrite comb_lin_scal.
Qed.
--
GitLab