chore(*): add mathlib4 synchronization comments (#18342)

Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following files: * `algebra.big_operators.associated` * `data.W.constructions` * `data.dlist.instances` * `data.multiset.functor` * `data.sign` * `data.sum.interval` * `group_theory.coset` * `topology.algebra.order.left_right` * `topology.constructions` * `topology.continuous_on` * `topology.inseparable` * `topology.local_extr` * `topology.maps` * `topology.order`
leanprover-community · Feb 1, 2023 · e46da4e · e46da4e
1 parent 832a8ba
commit e46da4e
Show file tree

Hide file tree

Showing 14 changed files with 42 additions and 0 deletions.
diff --git a/src/algebra/big_operators/associated.lean b/src/algebra/big_operators/associated.lean
@@ -10,6 +10,9 @@ import algebra.big_operators.finsupp
 /-!
 # Products of associated, prime, and irreducible elements.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file contains some theorems relating definitions in `algebra.associated`
 and products of multisets, finsets, and finsupps.
 

diff --git a/src/data/W/constructions.lean b/src/data/W/constructions.lean
@@ -8,6 +8,9 @@ import data.W.basic
 /-!
 # Examples of W-types
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We take the view of W types as inductive types.
 Given `α : Type` and `β : α → Type`, the W type determined by this data, `W_type β`, is the
 inductively with constructors from `α` and arities of each constructor `a : α` given by `β a`.

diff --git a/src/data/dlist/instances.lean b/src/data/dlist/instances.lean
@@ -9,6 +9,9 @@ import control.traversable.instances
 /-!
 # Traversable instance for dlists
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file provides the equivalence between `list α` and `dlist α` and the traversable instance
 for `dlist`.
 -/

diff --git a/src/data/multiset/functor.lean b/src/data/multiset/functor.lean
@@ -9,6 +9,9 @@ import control.traversable.instances
 
 /-!
 # Functoriality of `multiset`.
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 universes u

diff --git a/src/data/sign.lean b/src/data/sign.lean
@@ -11,6 +11,9 @@ import tactic.derive_fintype
 /-!
 # Sign function
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines the sign function for types with zero and a decidable less-than relation, and
 proves some basic theorems about it.
 -/

diff --git a/src/data/sum/interval.lean b/src/data/sum/interval.lean
@@ -9,6 +9,9 @@ import order.locally_finite
 /-!
 # Finite intervals in a disjoint union
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file provides the `locally_finite_order` instance for the disjoint sum of two orders.
 
 ## TODO

diff --git a/src/group_theory/coset.lean b/src/group_theory/coset.lean
@@ -13,6 +13,9 @@ import tactic.group
 /-!
 # Cosets
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file develops the basic theory of left and right cosets.
 
 ## Main definitions

diff --git a/src/topology/algebra/order/left_right.lean b/src/topology/algebra/order/left_right.lean
@@ -8,6 +8,9 @@ import topology.continuous_on
 /-!
 # Left and right continuity
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we prove a few lemmas about left and right continuous functions:
 
 * `continuous_within_at_Ioi_iff_Ici`: two definitions of right continuity

diff --git a/src/topology/constructions.lean b/src/topology/constructions.lean
@@ -10,6 +10,9 @@ import order.filter.pi
 /-!
 # Constructions of new topological spaces from old ones
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file constructs products, sums, subtypes and quotients of topological spaces
 and sets up their basic theory, such as criteria for maps into or out of these
 constructions to be continuous; descriptions of the open sets, neighborhood filters,

diff --git a/src/topology/continuous_on.lean b/src/topology/continuous_on.lean
@@ -8,6 +8,9 @@ import topology.constructions
 /-!
 # Neighborhoods and continuity relative to a subset
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines relative versions
 
 * `nhds_within`           of `nhds`

diff --git a/src/topology/inseparable.lean b/src/topology/inseparable.lean
@@ -10,6 +10,9 @@ import tactic.tfae
 /-!
 # Inseparable points in a topological space
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define
 
 * `specializes` (notation: `x ⤳ y`) : a relation saying that `𝓝 x ≤ 𝓝 y`;

diff --git a/src/topology/local_extr.lean b/src/topology/local_extr.lean
@@ -9,6 +9,9 @@ import topology.continuous_on
 /-!
 # Local extrema of functions on topological spaces
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Main definitions
 
 This file defines special versions of `is_*_filter f a l`, `*=min/max/extr`,

diff --git a/src/topology/maps.lean b/src/topology/maps.lean
@@ -9,6 +9,9 @@ import topology.nhds_set
 /-!
 # Specific classes of maps between topological spaces
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file introduces the following properties of a map `f : X → Y` between topological spaces:
 
 * `is_open_map f` means the image of an open set under `f` is open.

diff --git a/src/topology/order.lean b/src/topology/order.lean
@@ -8,6 +8,9 @@ import topology.tactic
 /-!
 # Ordering on topologies and (co)induced topologies
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Topologies on a fixed type `α` are ordered, by reverse inclusion.
 That is, for topologies `t₁` and `t₂` on `α`, we write `t₁ ≤ t₂`
 if every set open in `t₂` is also open in `t₁`.