chore: move pointwise set files to Algebra._.Pointwise

leanprover-community · Nov 16, 2024 · 586e58a · 586e58a
1 parent 2aeb155
commit 586e58a
Show file tree

Hide file tree

Showing 17 changed files with 18 additions and 45 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -289,7 +289,10 @@ import Mathlib.Algebra.Group.Pi.Lemmas
 import Mathlib.Algebra.Group.Pointwise.Finset.Basic
 import Mathlib.Algebra.Group.Pointwise.Finset.Interval
 import Mathlib.Algebra.Group.Pointwise.Set.Basic
+import Mathlib.Algebra.Group.Pointwise.Set.BigOperators
 import Mathlib.Algebra.Group.Pointwise.Set.Card
+import Mathlib.Algebra.Group.Pointwise.Set.Finite
+import Mathlib.Algebra.Group.Pointwise.Set.ListOfFn
 import Mathlib.Algebra.Group.Prod
 import Mathlib.Algebra.Group.Semiconj.Basic
 import Mathlib.Algebra.Group.Semiconj.Defs
@@ -648,6 +651,7 @@ import Mathlib.Algebra.Order.Group.OrderIso
 import Mathlib.Algebra.Order.Group.PiLex
 import Mathlib.Algebra.Order.Group.Pointwise.Bounds
 import Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
+import Mathlib.Algebra.Order.Group.Pointwise.Interval
 import Mathlib.Algebra.Order.Group.PosPart
 import Mathlib.Algebra.Order.Group.Prod
 import Mathlib.Algebra.Order.Group.Synonym
@@ -2797,12 +2801,7 @@ import Mathlib.Data.Set.Operations
 import Mathlib.Data.Set.Opposite
 import Mathlib.Data.Set.Pairwise.Basic
 import Mathlib.Data.Set.Pairwise.Lattice
-import Mathlib.Data.Set.Pointwise.BigOperators
-import Mathlib.Data.Set.Pointwise.BoundedMul
-import Mathlib.Data.Set.Pointwise.Finite
-import Mathlib.Data.Set.Pointwise.Interval
 import Mathlib.Data.Set.Pointwise.Iterate
-import Mathlib.Data.Set.Pointwise.ListOfFn
 import Mathlib.Data.Set.Pointwise.SMul
 import Mathlib.Data.Set.Pointwise.Support
 import Mathlib.Data.Set.Prod

diff --git a/Mathlib/Algebra/Algebra/Operations.lean b/Mathlib/Algebra/Algebra/Operations.lean
@@ -6,9 +6,9 @@ Authors: Kenny Lau
 import Mathlib.Algebra.Algebra.Bilinear
 import Mathlib.Algebra.Algebra.Opposite
 import Mathlib.Algebra.Group.Pointwise.Finset.Basic
+import Mathlib.Algebra.Group.Pointwise.Set.BigOperators
 import Mathlib.Algebra.GroupWithZero.NonZeroDivisors
 import Mathlib.Algebra.Module.Submodule.Pointwise
-import Mathlib.Data.Set.Pointwise.BigOperators
 import Mathlib.Data.Set.Semiring
 import Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise
 

diff --git a/Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean b/Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@@ -5,11 +5,11 @@ Authors: Floris van Doorn, Yaël Dillies
 -/
 import Mathlib.Algebra.BigOperators.Group.Finset
 import Mathlib.Algebra.Group.Action.Pi
+import Mathlib.Algebra.Group.Pointwise.Set.Finite
 import Mathlib.Data.Finset.Density
 import Mathlib.Data.Finset.Max
 import Mathlib.Data.Finset.NAry
-import Mathlib.Data.Set.Pointwise.Finite
-import Mathlib.Data.Set.Pointwise.ListOfFn
+import Mathlib.Algebra.Group.Pointwise.Set.ListOfFn
 import Mathlib.Data.Set.Pointwise.SMul
 
 /-!

diff --git a/Mathlib/Algebra/Group/Pointwise/Finset/Interval.lean b/Mathlib/Algebra/Group/Pointwise/Finset/Interval.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
 import Mathlib.Algebra.Group.Pointwise.Finset.Basic
-import Mathlib.Data.Set.Pointwise.Interval
+import Mathlib.Algebra.Order.Group.Pointwise.Interval
 import Mathlib.Order.Interval.Finset.Defs
 
 /-! # Pointwise operations on intervals

diff --git a/Mathlib/Data/Set/Pointwise/BigOperators.lean → ...bra/Group/Pointwise/Set/BigOperators.lean b/Mathlib/Data/Set/Pointwise/BigOperators.lean → ...bra/Group/Pointwise/Set/BigOperators.lean
diff --git a/Mathlib/Algebra/Group/Pointwise/Set/Card.lean b/Mathlib/Algebra/Group/Pointwise/Set/Card.lean
@@ -3,7 +3,7 @@ Copyright (c) 2024 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
-import Mathlib.Data.Set.Pointwise.Finite
+import Mathlib.Algebra.Group.Pointwise.Set.Finite
 import Mathlib.SetTheory.Cardinal.Finite
 
 /-!

diff --git a/Mathlib/Data/Set/Pointwise/Finite.lean → ...b/Algebra/Group/Pointwise/Set/Finite.lean b/Mathlib/Data/Set/Pointwise/Finite.lean → ...b/Algebra/Group/Pointwise/Set/Finite.lean
diff --git a/Mathlib/Data/Set/Pointwise/ListOfFn.lean → ...Algebra/Group/Pointwise/Set/ListOfFn.lean b/Mathlib/Data/Set/Pointwise/ListOfFn.lean → ...Algebra/Group/Pointwise/Set/ListOfFn.lean
diff --git a/Mathlib/Algebra/Order/Group/Pointwise/Bounds.lean b/Mathlib/Algebra/Order/Group/Pointwise/Bounds.lean
@@ -48,6 +48,8 @@ lemma BddAbove.mul (hs : BddAbove s) (ht : BddAbove t) : BddAbove (s * t) :=
 lemma BddBelow.mul (hs : BddBelow s) (ht : BddBelow t) : BddBelow (s * t) :=
   (Nonempty.mul hs ht).mono (subset_lowerBounds_mul s t)
 
+@[to_additive (attr := deprecated (since := "2024-11-13"))] alias Set.BddAbove.mul := BddAbove.mul
+
 @[to_additive]
 lemma BddAbove.range_mul (hf : BddAbove (range f)) (hg : BddAbove (range g)) :
     BddAbove (range fun i ↦ f i * g i) :=

diff --git a/Mathlib/Data/Set/Pointwise/Interval.lean → ...gebra/Order/Group/Pointwise/Interval.lean b/Mathlib/Data/Set/Pointwise/Interval.lean → ...gebra/Order/Group/Pointwise/Interval.lean
diff --git a/Mathlib/Analysis/Normed/Field/Basic.lean b/Mathlib/Analysis/Normed/Field/Basic.lean
@@ -5,10 +5,10 @@ Authors: Patrick Massot, Johannes Hölzl
 -/
 import Mathlib.Algebra.Algebra.NonUnitalSubalgebra
 import Mathlib.Algebra.Algebra.Subalgebra.Basic
+import Mathlib.Algebra.Field.Subfield.Defs
+import Mathlib.Algebra.Order.Group.Pointwise.Interval
 import Mathlib.Analysis.Normed.Group.Constructions
 import Mathlib.Analysis.Normed.Group.Submodule
-import Mathlib.Data.Set.Pointwise.Interval
-import Mathlib.Algebra.Field.Subfield.Defs
 
 /-!
 # Normed fields

diff --git a/Mathlib/Data/Real/Cardinality.lean b/Mathlib/Data/Real/Cardinality.lean
@@ -3,9 +3,9 @@ Copyright (c) 2019 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
+import Mathlib.Algebra.Order.Group.Pointwise.Interval
 import Mathlib.Analysis.SpecificLimits.Basic
 import Mathlib.Data.Rat.Denumerable
-import Mathlib.Data.Set.Pointwise.Interval
 import Mathlib.SetTheory.Cardinal.Continuum
 
 /-!

diff --git a/Mathlib/Data/Set/Pointwise/BoundedMul.lean b/Mathlib/Data/Set/Pointwise/BoundedMul.lean
diff --git a/Mathlib/GroupTheory/Finiteness.lean b/Mathlib/GroupTheory/Finiteness.lean
@@ -3,8 +3,8 @@ Copyright (c) 2021 Riccardo Brasca. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Riccardo Brasca
 -/
+import Mathlib.Algebra.Group.Pointwise.Set.Finite
 import Mathlib.Algebra.Group.Subgroup.Pointwise
-import Mathlib.Data.Set.Pointwise.Finite
 import Mathlib.GroupTheory.QuotientGroup.Defs
 import Mathlib.SetTheory.Cardinal.Finite
 

diff --git a/Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean b/Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Joseph Myers. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Myers
 -/
-import Mathlib.Data.Set.Pointwise.Interval
+import Mathlib.Algebra.Order.Group.Pointwise.Interval
 import Mathlib.LinearAlgebra.AffineSpace.Basic
 import Mathlib.LinearAlgebra.BilinearMap
 import Mathlib.LinearAlgebra.Pi

diff --git a/Mathlib/Topology/Algebra/Order/Field.lean b/Mathlib/Topology/Algebra/Order/Field.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Benjamin Davidson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Benjamin Davidson, Devon Tuma, Eric Rodriguez, Oliver Nash
 -/
-import Mathlib.Data.Set.Pointwise.Interval
+import Mathlib.Algebra.Order.Group.Pointwise.Interval
 import Mathlib.Order.Filter.AtTopBot.Field
 import Mathlib.Topology.Algebra.Field
 import Mathlib.Topology.Algebra.Order.Group

diff --git a/Mathlib/Topology/MetricSpace/Pseudo/Real.lean b/Mathlib/Topology/MetricSpace/Pseudo/Real.lean
@@ -3,7 +3,7 @@ Copyright (c) 2015, 2017 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Robert Y. Lewis, Johannes Hölzl, Mario Carneiro, Sébastien Gouëzel
 -/
-import Mathlib.Data.Set.Pointwise.Interval
+import Mathlib.Algebra.Order.Group.Pointwise.Interval
 import Mathlib.Topology.MetricSpace.Pseudo.Pi
 
 /-!