diff --git a/CHANGELOG.md b/CHANGELOG.md
index 8106f8d2cca21bddc3c21f2cd2f4ef095b3dbd7a..1c0b56f1c9a69513be0eec4c55064530124bcfc9 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -9,6 +9,18 @@ API-breaking change is listed.
   `head_app_Some`, `head_app_None` and `head_app`. (by Marijn van Wezel)
 - Add tactic `notypeclasses apply` that works like `notypeclasses refine` but
   automatically adds `_` until the given lemma takes no more arguments.
+- Rename `map_filter_empty_iff` to `map_empty_filter` and add
+  `map_empty_filter_1` and `map_empty_filter_2`. (by Michael Sammler)
+
+The following `sed` script should perform most of the renaming
+(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
+Note that the script is not idempotent, do not run it twice.
+```
+sed -i -E -f- $(find theories -name "*.v") <<EOF
+# length
+s/\bmap_filter_empty_iff\b/map_empty_filter/g
+EOF
+```
 
 ## std++ 1.11.0 (2024-10-30)
 
diff --git a/stdpp/fin_maps.v b/stdpp/fin_maps.v
index 655699127f7973727caaeea8aa885b7fe7ba22bb..c8aabceddbf77ad474e143abde8400cf347f5b30 100644
--- a/stdpp/fin_maps.v
+++ b/stdpp/fin_maps.v
@@ -1858,7 +1858,7 @@ Section map_filter.
 
   Lemma map_filter_empty : filter P ∅ =@{M A} ∅.
   Proof. apply map_fold_empty. Qed.
-  Lemma map_filter_empty_iff m :
+  Lemma map_empty_filter m :
     filter P m = ∅ ↔ map_Forall (λ i x, ¬P (i,x)) m.
   Proof.
     rewrite map_empty. setoid_rewrite map_lookup_filter_None. split.
@@ -1866,6 +1866,14 @@ Section map_filter.
     - intros Hm i. destruct (m !! i) as [x|] eqn:?; [|by auto].
       right; intros ? [= <-]. by apply Hm.
   Qed.
+  Lemma map_empty_filter_1 m :
+    filter P m = ∅ →
+    map_Forall (λ i x, ¬P (i,x)) m.
+  Proof. apply map_empty_filter. Qed.
+  Lemma map_empty_filter_2 m :
+    map_Forall (λ i x, ¬P (i,x)) m →
+    filter P m = ∅.
+  Proof. apply map_empty_filter. Qed.
 
   Lemma map_filter_delete m i : filter P (delete i m) = delete i (filter P m).
   Proof.