From 42644d144efdc96b56e9b31d7525a93800c389ce Mon Sep 17 00:00:00 2001 From: YaelDillies Date: Wed, 15 Mar 2023 09:00:57 +0000 Subject: [PATCH 1/3] chore: Fix `Topology.Algebra.Order.UpperLower` docstring --- Mathlib/Topology/Algebra/Order/UpperLower.lean | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/Mathlib/Topology/Algebra/Order/UpperLower.lean b/Mathlib/Topology/Algebra/Order/UpperLower.lean index cbe20b302a473..be1d90529ecb3 100644 --- a/Mathlib/Topology/Algebra/Order/UpperLower.lean +++ b/Mathlib/Topology/Algebra/Order/UpperLower.lean @@ -18,11 +18,10 @@ The topological closure and interior of an upper/lower/order-connected set is an upper/lower/order-connected set (with the notable exception of the closure of an order-connected set). -## Notes +## Implementation notes -The lemmas don't mention additive/multiplicative operations. As a result, we decide to prime the -multiplicative lemma names to indicate that there is probably a common generalisation to each pair -of additive/multiplicative lemma. +The same lemmas are true in the additive/multiplicative worlds. To avoid code duplication, we +provide `has_upper_lower_closure`, an ad hoc axiomatisation of the properties we need. -/ From d164a985e34fb67b9ef15bb846769f5c02d2a6a1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Wed, 15 Mar 2023 10:13:40 +0100 Subject: [PATCH 2/3] fix docs Co-authored-by: Jeremy Tan Jie Rui --- Mathlib/Topology/Algebra/Order/UpperLower.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Topology/Algebra/Order/UpperLower.lean b/Mathlib/Topology/Algebra/Order/UpperLower.lean index be1d90529ecb3..9c2ed79fdb200 100644 --- a/Mathlib/Topology/Algebra/Order/UpperLower.lean +++ b/Mathlib/Topology/Algebra/Order/UpperLower.lean @@ -21,7 +21,7 @@ set). ## Implementation notes The same lemmas are true in the additive/multiplicative worlds. To avoid code duplication, we -provide `has_upper_lower_closure`, an ad hoc axiomatisation of the properties we need. +provide `HasUpperLowerClosure`, an ad hoc axiomatisation of the properties we need. -/ From 9b9f521891f6f3c2d4ade7c51e9378d65f2e5cc7 Mon Sep 17 00:00:00 2001 From: Jeremy Tan Jie Rui Date: Tue, 21 Mar 2023 08:46:57 +0800 Subject: [PATCH 3/3] =?UTF-8?q?=D0=A8?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Mathlib/Topology/Algebra/Order/UpperLower.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Topology/Algebra/Order/UpperLower.lean b/Mathlib/Topology/Algebra/Order/UpperLower.lean index 9c2ed79fdb200..ccfc49336bcf3 100644 --- a/Mathlib/Topology/Algebra/Order/UpperLower.lean +++ b/Mathlib/Topology/Algebra/Order/UpperLower.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Yaël Dillies ! This file was ported from Lean 3 source module topology.algebra.order.upper_lower -! leanprover-community/mathlib commit 4330aae21f538b862f8aead371cfb6ee556398f1 +! leanprover-community/mathlib commit 992efbda6f85a5c9074375d3c7cb9764c64d8f72 ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/