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

Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following files: * `combinatorics.simple_graph.regularity.equitabilise` * `data.dfinsupp.interval` * `data.finsupp.interval` * `data.set.mul_antidiagonal` * `group_theory.divisible` * `linear_algebra.affine_space.basic` * `order.upper_lower.hom` * `ring_theory.ore_localization.basic` * `topology.algebra.order.liminf_limsup` * `topology.filter` * `topology.order.hom.basic`
leanprover-community · Feb 9, 2023 · b6da1a0 · b6da1a0
1 parent 38d38e0
commit b6da1a0
Show file tree

Hide file tree

Showing 11 changed files with 34 additions and 1 deletion.
diff --git a/src/combinatorics/simple_graph/regularity/equitabilise.lean b/src/combinatorics/simple_graph/regularity/equitabilise.lean
@@ -8,6 +8,9 @@ import order.partition.equipartition
 /-!
 # Equitabilising a partition
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file allows to blow partitions up into parts of controlled size. Given a partition `P` and
 `a b m : ℕ`, we want to find a partition `Q` with `a` parts of size `m` and `b` parts of size
 `m + 1` such that all parts of `P` are "as close as possible" to unions of parts of `Q`. By

diff --git a/src/data/dfinsupp/interval.lean b/src/data/dfinsupp/interval.lean
@@ -11,6 +11,9 @@ import data.dfinsupp.order
 /-!
 # Finite intervals of finitely supported functions
 
+> 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 `Π₀ i, α i` when `α` itself is locally
 finite and calculates the cardinality of its finite intervals.
 -/

diff --git a/src/data/finsupp/interval.lean b/src/data/finsupp/interval.lean
@@ -10,6 +10,9 @@ import data.finsupp.order
 /-!
 # Finite intervals of finitely supported functions
 
+> 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 `ι →₀ α` when `α` itself is locally
 finite and calculates the cardinality of its finite intervals.
 

diff --git a/src/data/set/mul_antidiagonal.lean b/src/data/set/mul_antidiagonal.lean
@@ -5,7 +5,10 @@ Authors: Johan Commelin, Floris van Doorn
 -/
 import order.well_founded_set
 
-/-! # Multiplication antidiagonal -/
+/-! # Multiplication antidiagonal 
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.-/
 
 namespace set
 variables {α : Type*}

diff --git a/src/group_theory/divisible.lean b/src/group_theory/divisible.lean
@@ -10,6 +10,9 @@ import algebra.group.pi
 /-!
 # Divisible Group and rootable group
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file, we define a divisible add monoid and a rootable monoid with some basic properties.
 
 ## Main definition

diff --git a/src/linear_algebra/affine_space/basic.lean b/src/linear_algebra/affine_space/basic.lean
@@ -8,6 +8,9 @@ import algebra.add_torsor
 /-!
 # Affine space
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we introduce the following notation:
 
 * `affine_space V P` is an alternative notation for `add_torsor V P` introduced at the end of this

diff --git a/src/order/upper_lower/hom.lean b/src/order/upper_lower/hom.lean
@@ -9,6 +9,9 @@ import order.hom.complete_lattice
 /-!
 # `upper_set.Ici` etc as `sup`/`Sup`/`inf`/`Inf`-homomorphisms
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define `upper_set.Ici_sup_hom` etc. These functions are `upper_set.Ici` and
 `lower_set.Iic` bundled as `sup_hom`s, `inf_hom`s, `Sup_hom`s, or `Inf_hom`s.
 -/

diff --git a/src/ring_theory/ore_localization/basic.lean b/src/ring_theory/ore_localization/basic.lean
@@ -12,6 +12,9 @@ import tactic.noncomm_ring
 
 # Localization over right Ore sets.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines the localization of a monoid over a right Ore set and proves its universal
 mapping property. It then extends the definition and its properties first to semirings and then
 to rings. We show that in the case of a commutative monoid this definition coincides with the

diff --git a/src/topology/algebra/order/liminf_limsup.lean b/src/topology/algebra/order/liminf_limsup.lean
@@ -12,6 +12,9 @@ import topology.order.basic
 
 /-!
 # Lemmas about liminf and limsup in an order topology.
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 open filter

diff --git a/src/topology/filter.lean b/src/topology/filter.lean
@@ -10,6 +10,9 @@ import data.set.intervals.monotone
 /-!
 # Topology on the set of filters on a type
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file introduce topology on `filter α`. It is generated by the sets
 `set.Iic (𝓟 s) = {l : filter α | s ∈ l}`, `s : set α`. A set `s : set (filter α)` is open if and
 only if it is a union of a family of these basic open sets, see `filter.is_open_iff`.

diff --git a/src/topology/order/hom/basic.lean b/src/topology/order/hom/basic.lean
@@ -9,6 +9,9 @@ import topology.continuous_function.basic
 /-!
 # Continuous order homomorphisms
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines continuous order homomorphisms, that is maps which are both continuous and
 monotone. They are also called Priestley homomorphisms because they are the morphisms of the
 category of Priestley spaces.