From 88abdc7699c1d16ea604361fe7120b14c2fb4d0b Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Sun, 26 Feb 2023 14:27:12 +0100 Subject: [PATCH 1/4] feat: port Topology.Algebra.Order.UpperLower From 9b367b222d01009d8da3062281a8c8199b1045d5 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Sun, 26 Feb 2023 14:27:12 +0100 Subject: [PATCH 2/4] Initial file copy from mathport --- .../Topology/Algebra/Order/UpperLower.lean | 124 ++++++++++++++++++ 1 file changed, 124 insertions(+) create mode 100644 Mathlib/Topology/Algebra/Order/UpperLower.lean diff --git a/Mathlib/Topology/Algebra/Order/UpperLower.lean b/Mathlib/Topology/Algebra/Order/UpperLower.lean new file mode 100644 index 0000000000000..7be79c456a201 --- /dev/null +++ b/Mathlib/Topology/Algebra/Order/UpperLower.lean @@ -0,0 +1,124 @@ +/- +Copyright (c) 2022 Yaël Dillies. All rights reserved. +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 +! Please do not edit these lines, except to modify the commit id +! if you have ported upstream changes. +-/ +import Mathbin.Algebra.Order.UpperLower +import Mathbin.Topology.Algebra.Group.Basic + +/-! +# Topological facts about upper/lower/order-connected sets + +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 + +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. +-/ + + +open Function Set + +open Pointwise + +/-- Ad hoc class stating that the closure of an upper set is an upper set. This is used to state +lemmas that do not mention algebraic operations for both the additive and multiplicative versions +simultaneously. If you find a satisfying replacement for this typeclass, please remove it! -/ +class HasUpperLowerClosure (α : Type _) [TopologicalSpace α] [Preorder α] : Prop where + isUpperSet_closure : ∀ s : Set α, IsUpperSet s → IsUpperSet (closure s) + isLowerSet_closure : ∀ s : Set α, IsLowerSet s → IsLowerSet (closure s) + isOpen_upperClosure : ∀ s : Set α, IsOpen s → IsOpen (upperClosure s : Set α) + isOpen_lowerClosure : ∀ s : Set α, IsOpen s → IsOpen (lowerClosure s : Set α) +#align has_upper_lower_closure HasUpperLowerClosure + +variable {α : Type _} [TopologicalSpace α] + +-- See note [lower instance priority] +@[to_additive] +instance (priority := 100) OrderedCommGroup.to_hasUpperLowerClosure [OrderedCommGroup α] + [ContinuousConstSMul α α] : HasUpperLowerClosure α + where + isUpperSet_closure s h x y hxy hx := + closure_mono (h.smul_subset <| one_le_div'.2 hxy) <| + by + rw [closure_smul] + exact ⟨x, hx, div_mul_cancel' _ _⟩ + isLowerSet_closure s h x y hxy hx := + closure_mono (h.smul_subset <| div_le_one'.2 hxy) <| + by + rw [closure_smul] + exact ⟨x, hx, div_mul_cancel' _ _⟩ + isOpen_upperClosure s hs := by + rw [← mul_one s, ← mul_upperClosure] + exact hs.mul_right + isOpen_lowerClosure s hs := by + rw [← mul_one s, ← mul_lowerClosure] + exact hs.mul_right +#align ordered_comm_group.to_has_upper_lower_closure OrderedCommGroup.to_hasUpperLowerClosure +#align ordered_add_comm_group.to_has_upper_lower_closure OrderedAddCommGroup.to_hasUpperLowerClosure + +variable [Preorder α] [HasUpperLowerClosure α] {s : Set α} + +protected theorem IsUpperSet.closure : IsUpperSet s → IsUpperSet (closure s) := + HasUpperLowerClosure.isUpperSet_closure _ +#align is_upper_set.closure IsUpperSet.closure + +protected theorem IsLowerSet.closure : IsLowerSet s → IsLowerSet (closure s) := + HasUpperLowerClosure.isLowerSet_closure _ +#align is_lower_set.closure IsLowerSet.closure + +protected theorem IsOpen.upperClosure : IsOpen s → IsOpen (upperClosure s : Set α) := + HasUpperLowerClosure.isOpen_upperClosure _ +#align is_open.upper_closure IsOpen.upperClosure + +protected theorem IsOpen.lowerClosure : IsOpen s → IsOpen (lowerClosure s : Set α) := + HasUpperLowerClosure.isOpen_lowerClosure _ +#align is_open.lower_closure IsOpen.lowerClosure + +instance : HasUpperLowerClosure αᵒᵈ + where + isUpperSet_closure := @IsLowerSet.closure α _ _ _ + isLowerSet_closure := @IsUpperSet.closure α _ _ _ + isOpen_upperClosure := @IsOpen.lowerClosure α _ _ _ + isOpen_lowerClosure := @IsOpen.upperClosure α _ _ _ + +/- +Note: `s.ord_connected` does not imply `(closure s).ord_connected`, as we can see by taking +`s := Ioo 0 1 × Ioo 1 2 ∪ Ioo 2 3 × Ioo 0 1` because then +`closure s = Icc 0 1 × Icc 1 2 ∪ Icc 2 3 × Icc 0 1` is not order-connected as +`(1, 1) ∈ closure s`, `(2, 1) ∈ closure s` but `Icc (1, 1) (2, 1) ⊈ closure s`. + +`s` looks like +``` +xxooooo +xxooooo +oooooxx +oooooxx +``` +-/ +protected theorem IsUpperSet.interior (h : IsUpperSet s) : IsUpperSet (interior s) := + by + rw [← isLowerSet_compl, ← closure_compl] + exact h.compl.closure +#align is_upper_set.interior IsUpperSet.interior + +protected theorem IsLowerSet.interior (h : IsLowerSet s) : IsLowerSet (interior s) := + h.ofDual.interior +#align is_lower_set.interior IsLowerSet.interior + +protected theorem Set.OrdConnected.interior (h : s.OrdConnected) : (interior s).OrdConnected := + by + rw [← h.upper_closure_inter_lower_closure, interior_inter] + exact + (upperClosure s).upper.interior.OrdConnected.inter (lowerClosure s).lower.interior.OrdConnected +#align set.ord_connected.interior Set.OrdConnected.interior + From 3e29cc80c87f639c2e4a998bf3828f38aaf6dabd Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Sun, 26 Feb 2023 14:27:12 +0100 Subject: [PATCH 3/4] automated fixes Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean --- Mathlib.lean | 1 + Mathlib/Topology/Algebra/Order/UpperLower.lean | 10 ++++------ 2 files changed, 5 insertions(+), 6 deletions(-) diff --git a/Mathlib.lean b/Mathlib.lean index 8edf9b49cc0f6..1c7da8bc8bae5 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -1184,6 +1184,7 @@ import Mathlib.Topology.Algebra.Order.MonotoneContinuity import Mathlib.Topology.Algebra.Order.MonotoneConvergence import Mathlib.Topology.Algebra.Order.ProjIcc import Mathlib.Topology.Algebra.Order.T5 +import Mathlib.Topology.Algebra.Order.UpperLower import Mathlib.Topology.Algebra.Semigroup import Mathlib.Topology.Algebra.Star import Mathlib.Topology.Bases diff --git a/Mathlib/Topology/Algebra/Order/UpperLower.lean b/Mathlib/Topology/Algebra/Order/UpperLower.lean index 7be79c456a201..d97da51fc78fa 100644 --- a/Mathlib/Topology/Algebra/Order/UpperLower.lean +++ b/Mathlib/Topology/Algebra/Order/UpperLower.lean @@ -8,8 +8,8 @@ Authors: Yaël Dillies ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ -import Mathbin.Algebra.Order.UpperLower -import Mathbin.Topology.Algebra.Group.Basic +import Mathlib.Algebra.Order.UpperLower +import Mathlib.Topology.Algebra.Group.Basic /-! # Topological facts about upper/lower/order-connected sets @@ -105,8 +105,7 @@ oooooxx oooooxx ``` -/ -protected theorem IsUpperSet.interior (h : IsUpperSet s) : IsUpperSet (interior s) := - by +protected theorem IsUpperSet.interior (h : IsUpperSet s) : IsUpperSet (interior s) := by rw [← isLowerSet_compl, ← closure_compl] exact h.compl.closure #align is_upper_set.interior IsUpperSet.interior @@ -115,8 +114,7 @@ protected theorem IsLowerSet.interior (h : IsLowerSet s) : IsLowerSet (interior h.ofDual.interior #align is_lower_set.interior IsLowerSet.interior -protected theorem Set.OrdConnected.interior (h : s.OrdConnected) : (interior s).OrdConnected := - by +protected theorem Set.OrdConnected.interior (h : s.OrdConnected) : (interior s).OrdConnected := by rw [← h.upper_closure_inter_lower_closure, interior_inter] exact (upperClosure s).upper.interior.OrdConnected.inter (lowerClosure s).lower.interior.OrdConnected From 95ea007e6894b68239096c81636be96c502cd590 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Sun, 26 Feb 2023 15:35:36 +0100 Subject: [PATCH 4/4] first pass --- Mathlib/GroupTheory/GroupAction/Opposite.lean | 2 ++ Mathlib/Topology/Algebra/Order/UpperLower.lean | 7 +++---- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/Mathlib/GroupTheory/GroupAction/Opposite.lean b/Mathlib/GroupTheory/GroupAction/Opposite.lean index 171a7102a741a..31d46ca9b116d 100644 --- a/Mathlib/GroupTheory/GroupAction/Opposite.lean +++ b/Mathlib/GroupTheory/GroupAction/Opposite.lean @@ -126,9 +126,11 @@ instance Semigroup.opposite_smulCommClass' [Semigroup α] : SMulCommClass α α #align semigroup.opposite_smul_comm_class' Semigroup.opposite_smulCommClass' #align add_semigroup.opposite_vadd_comm_class' AddSemigroup.opposite_vaddCommClass' +@[to_additive] instance CommSemigroup.isCentralScalar [CommSemigroup α] : IsCentralScalar α α := ⟨fun _ _ => mul_comm _ _⟩ #align comm_semigroup.is_central_scalar CommSemigroup.isCentralScalar +#align add_comm_semigroup.is_central_scalar AddCommSemigroup.isCentralScalar /-- Like `Monoid.toMulAction`, but multiplies on the right. -/ @[to_additive "Like `AddMonoid.toAddAction`, but adds on the right."] diff --git a/Mathlib/Topology/Algebra/Order/UpperLower.lean b/Mathlib/Topology/Algebra/Order/UpperLower.lean index d97da51fc78fa..cbe20b302a473 100644 --- a/Mathlib/Topology/Algebra/Order/UpperLower.lean +++ b/Mathlib/Topology/Algebra/Order/UpperLower.lean @@ -92,7 +92,7 @@ instance : HasUpperLowerClosure αᵒᵈ isOpen_lowerClosure := @IsOpen.upperClosure α _ _ _ /- -Note: `s.ord_connected` does not imply `(closure s).ord_connected`, as we can see by taking +Note: `s.OrdConnected` does not imply `(closure s).OrdConnected`, as we can see by taking `s := Ioo 0 1 × Ioo 1 2 ∪ Ioo 2 3 × Ioo 0 1` because then `closure s = Icc 0 1 × Icc 1 2 ∪ Icc 2 3 × Icc 0 1` is not order-connected as `(1, 1) ∈ closure s`, `(2, 1) ∈ closure s` but `Icc (1, 1) (2, 1) ⊈ closure s`. @@ -115,8 +115,7 @@ protected theorem IsLowerSet.interior (h : IsLowerSet s) : IsLowerSet (interior #align is_lower_set.interior IsLowerSet.interior protected theorem Set.OrdConnected.interior (h : s.OrdConnected) : (interior s).OrdConnected := by - rw [← h.upper_closure_inter_lower_closure, interior_inter] + rw [← h.upperClosure_inter_lowerClosure, interior_inter] exact - (upperClosure s).upper.interior.OrdConnected.inter (lowerClosure s).lower.interior.OrdConnected + (upperClosure s).upper.interior.ordConnected.inter (lowerClosure s).lower.interior.ordConnected #align set.ord_connected.interior Set.OrdConnected.interior -