From e5571d04a2e789b8945dda4ec7156277998201f9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Tue, 30 Jan 2024 23:19:01 +0100
Subject: [PATCH] Rename filterP_ord_incrF -> filterP_ord_w_incrF,
filterP_f_ord_incrF -> filterP_f_ord_w_incrF.
---
FEM/Algebra/Finite_family.v | 8 ++++----
1 file changed, 4 insertions(+), 4 deletions(-)
diff --git a/FEM/Algebra/Finite_family.v b/FEM/Algebra/Finite_family.v
index af9185d6..2de3be34 100644
--- a/FEM/Algebra/Finite_family.v
+++ b/FEM/Algebra/Finite_family.v
@@ -4856,7 +4856,7 @@ apply sym_eq, Rg_0_liftF_S.
rewrite Rg_0_liftF_S; f_equal; rewrite Y1; easy.
Qed.
-Lemma filterP_ord_incrF :
+Lemma filterP_ord_w_incrF :
forall {n1 n2} {f : 'I_{n1,n2}} (Hf : incrF f) {P1 : 'Prop^n1}
{P2 : 'Prop^n2} (HP : extendPF f P1 P2),
let H := lenPF_extendPF (incrF_inj Hf) HP in
@@ -4868,7 +4868,7 @@ apply filterP_cast_ord_incrF.
apply filterP_ord_Rg.
Qed.
-Lemma filterP_f_ord_incrF :
+Lemma filterP_f_ord_w_incrF :
forall {n1 n2} {f : 'I_{n1,n2}} (Hf : incrF f)
{P1 : 'Prop^n1} {P2 : 'Prop^n2} (HP : extendPF f P1 P2)
{i1} (HP2 : P2 (f i1)),
@@ -4878,7 +4878,7 @@ Proof.
intros n1 n2 f Hf P1 P2 HP i1 HP2 H; apply extF; intros j1.
move: (extendPF_unfunF_rev (incrF_inj Hf) HP) => HP2'; subst.
rewrite (filterP_f_ord_correct_alt _ (incrF_inj Hf) HP) -(comp_correct _ f).
-rewrite (filterP_ord_incrF Hf HP); easy.
+rewrite (filterP_ord_w_incrF Hf HP); easy.
Qed.
(* Was:
@@ -4975,7 +4975,7 @@ rewrite (filterPF_permutF HP1' Hq1b) -{2}(funF_unfunF x0 Hf A1).
rewrite (filterPF_funF HP2' Hf HP).
apply extF; intros j2; unfold castF, funF; f_equal.
rewrite -(filterP_f_ord_comp_l HP1' Hq1b).
-rewrite (filterP_f_ord_incrF Hq1c (extendPF_incrF Hf HP)).
+rewrite (filterP_f_ord_w_incrF Hq1c (extendPF_incrF Hf HP)).
rewrite 2!cast_ord_comp cast_ord_id; easy.
Qed.
--
GitLab