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

github-actions[bot] · github-actions[bot] · commit 0a0ec35061ed · 2023-02-06T06:28:11.000Z
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following files: * `combinatorics.colex` * `combinatorics.set_family.harris_kleitman` * `data.finset.pimage` * `data.fintype.perm` * `data.holor` * `dynamics.minimal` * `order.filter.partial` * `order.partition.equipartition` * `order.partition.finpartition` * `topology.extend_from` * `topology.order.basic` * `topology.paracompact` * `topology.shrinking_lemma` * `topology.uniform_space.absolute_value` * `topology.uniform_space.complete_separated` * `topology.uniform_space.pi` * `topology.uniform_space.uniform_convergence` * `topology.uniform_space.uniform_embedding`
diff --git a/src/combinatorics/colex.lean b/src/combinatorics/colex.lean
@@ -9,6 +9,9 @@ import algebra.geom_sum
 /-!
 # Colex
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We define the colex ordering for finite sets, and give a couple of important
 lemmas and properties relating to it.
 
diff --git a/src/combinatorics/set_family/harris_kleitman.lean b/src/combinatorics/set_family/harris_kleitman.lean
@@ -10,6 +10,9 @@ import data.fintype.big_operators
 /-!
 # Harris-Kleitman inequality
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file proves the Harris-Kleitman inequality. This relates `𝒜.card * ℬ.card` and
 `2 ^ card α * (𝒜 ∩ ℬ).card` where `𝒜` and `ℬ` are upward- or downcard-closed finite families of
 finsets. This can be interpreted as saying that any two lower sets (resp. any two upper sets)
diff --git a/src/data/finset/pimage.lean b/src/data/finset/pimage.lean
@@ -9,6 +9,9 @@ import data.pfun
 /-!
 # Image of a `finset α` under a partially defined function
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define `part.to_finset` and `finset.pimage`. We also prove some trivial lemmas about
 these definitions.
 
diff --git a/src/data/fintype/perm.lean b/src/data/fintype/perm.lean
@@ -9,6 +9,9 @@ import group_theory.perm.basic
 /-!
 # fintype instances for `equiv` and `perm`
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Main declarations:
 * `perms_of_finset s`: The finset of permutations of the finset `s`.
 
diff --git a/src/data/holor.lean b/src/data/holor.lean
@@ -9,6 +9,9 @@ import algebra.big_operators.basic
 /-!
 # Basic properties of holors
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Holors are indexed collections of tensor coefficients. Confusingly,
 they are often called tensors in physics and in the neural network
 community.
diff --git a/src/dynamics/minimal.lean b/src/dynamics/minimal.lean
@@ -9,6 +9,9 @@ import topology.algebra.const_mul_action
 /-!
 # Minimal action of a group
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define an action of a monoid `M` on a topological space `α` to be *minimal* if the
 `M`-orbit of every point `x : α` is dense. We also provide an additive version of this definition
 and prove some basic facts about minimal actions.
diff --git a/src/order/filter/partial.lean b/src/order/filter/partial.lean
@@ -9,6 +9,9 @@ import data.pfun
 /-!
 # `tendsto` for relations and partial functions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file generalizes `filter` definitions from functions to partial functions and relations.
 
 ## Considering functions and partial functions as relations
diff --git a/src/order/partition/equipartition.lean b/src/order/partition/equipartition.lean
@@ -9,6 +9,9 @@ import order.partition.finpartition
 /-!
 # Finite equipartitions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines finite equipartitions, the partitions whose parts all are the same size up to a
 difference of `1`.
 
diff --git a/src/order/partition/finpartition.lean b/src/order/partition/finpartition.lean
@@ -10,6 +10,9 @@ import order.sup_indep
 /-!
 # Finite partitions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file, we define finite partitions. A finpartition of `a : α` is a finite set of pairwise
 disjoint parts `parts : finset α` which does not contain `⊥` and whose supremum is `a`.
 
diff --git a/src/topology/extend_from.lean b/src/topology/extend_from.lean
@@ -8,6 +8,9 @@ import topology.separation
 /-!
 # Extending a function from a subset
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The main definition of this file is `extend_from A f` where `f : X → Y`
 and `A : set X`. This defines a new function `g : X → Y` which maps any
 `x₀ : X` to the limit of `f` as `x` tends to `x₀`, if such a limit exists.
diff --git a/src/topology/order/basic.lean b/src/topology/order/basic.lean
@@ -12,6 +12,9 @@ import topology.algebra.order.left_right
 /-!
 # Theory of topology on ordered spaces
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Main definitions
 
 The order topology on an ordered space is the topology generated by all open intervals (or
diff --git a/src/topology/paracompact.lean b/src/topology/paracompact.lean
@@ -10,6 +10,9 @@ import data.option.basic
 /-!
 # Paracompact topological spaces
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A topological space `X` is said to be paracompact if every open covering of `X` admits a locally
 finite refinement.
 
diff --git a/src/topology/shrinking_lemma.lean b/src/topology/shrinking_lemma.lean
@@ -8,6 +8,9 @@ import topology.separation
 /-!
 # The shrinking lemma
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we prove a few versions of the shrinking lemma. The lemma says that in a normal
 topological space a point finite open covering can be “shrunk”: for a point finite open covering
 `u : ι → set X` there exists a refinement `v : ι → set X` such that `closure (v i) ⊆ u i`.
diff --git a/src/topology/uniform_space/absolute_value.lean b/src/topology/uniform_space/absolute_value.lean
@@ -9,6 +9,9 @@ import topology.uniform_space.basic
 /-!
 # Uniform structure induced by an absolute value
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We build a uniform space structure on a commutative ring `R` equipped with an absolute value into
 a linear ordered field `𝕜`. Of course in the case `R` is `ℚ`, `ℝ` or `ℂ` and
 `𝕜 = ℝ`, we get the same thing as the metric space construction, and the general construction
diff --git a/src/topology/uniform_space/complete_separated.lean b/src/topology/uniform_space/complete_separated.lean
@@ -10,6 +10,9 @@ import topology.dense_embedding
 /-!
 # Theory of complete separated uniform spaces.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file is for elementary lemmas that depend on both Cauchy filters and separation.
 -/
 
diff --git a/src/topology/uniform_space/pi.lean b/src/topology/uniform_space/pi.lean
@@ -8,6 +8,9 @@ import topology.uniform_space.separation
 
 /-!
 # Indexed product of uniform spaces
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 noncomputable theory
diff --git a/src/topology/uniform_space/uniform_convergence.lean b/src/topology/uniform_space/uniform_convergence.lean
@@ -10,6 +10,9 @@ import topology.uniform_space.cauchy
 /-!
 # Uniform convergence
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A sequence of functions `Fₙ` (with values in a metric space) converges uniformly on a set `s` to a
 function `f` if, for all `ε > 0`, for all large enough `n`, one has for all `y ∈ s` the inequality
 `dist (f y, Fₙ y) < ε`. Under uniform convergence, many properties of the `Fₙ` pass to the limit,
diff --git a/src/topology/uniform_space/uniform_embedding.lean b/src/topology/uniform_space/uniform_embedding.lean
@@ -10,6 +10,9 @@ import topology.dense_embedding
 /-!
 # Uniform embeddings of uniform spaces.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Extension of uniform continuous functions.
 -/
 
