From 10d11277cadc467ad03684f6da5fec493f4a102a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 31 Mar 2020 23:51:45 +0200
Subject: [PATCH] =?UTF-8?q?Prove=20that=20`=E2=89=A1`=20is=20limit=20prese?=
 =?UTF-8?q?rving.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/algebra/ofe.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 777559a15..7a1407ffa 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -289,6 +289,13 @@ Section limit_preserving.
     (∀ y, LimitPreserving (P y)) →
     LimitPreserving (λ x, ∀ y, P y x).
   Proof. intros Hlim c Hc y. by apply Hlim. Qed.
+
+  Lemma limit_preserving_equiv `{!Cofe B} (f g : A → B) :
+    NonExpansive f → NonExpansive g → LimitPreserving (λ x, f x ≡ g x).
+  Proof.
+    intros Hf Hg c Hc. apply equiv_dist=> n.
+    by rewrite -!compl_chain_map !conv_compl /= Hc.
+  Qed.
 End limit_preserving.
 
 (** Fixpoint *)
-- 
GitLab