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

github-actions[bot] · github-actions[bot] · commit 4c19a16e4b70 · 2023-02-04T09:12: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.set_family.compression.uv` * `combinatorics.young.young_diagram` * `data.finmap` * `data.finsupp.multiset` * `data.finsupp.to_dfinsupp` * `data.fp.basic` * `data.set_like.fintype` * `dynamics.fixed_points.topology` * `linear_algebra.general_linear_group` * `order.countable_dense_linear_order` * `order.hom.lattice` * `order.succ_pred.linear_locally_finite` * `topology.omega_complete_partial_order` * `topology.uniform_space.cauchy` * `topology.uniform_space.separation`
diff --git a/src/combinatorics/set_family/compression/uv.lean b/src/combinatorics/set_family/compression/uv.lean
@@ -8,6 +8,9 @@ import data.finset.card
 /-!
 # UV-compressions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines UV-compression. It is an operation on a set family that reduces its shadow.
 
 UV-compressing `a : α` along `u v : α` means replacing `a` by `(a ⊔ u) \ v` if `a` and `u` are
diff --git a/src/combinatorics/young/young_diagram.lean b/src/combinatorics/young/young_diagram.lean
@@ -9,6 +9,9 @@ import data.finset.preimage
 /-!
 # Young diagrams
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A Young diagram is a finite set of up-left justified boxes:
 
 ```text
diff --git a/src/data/finmap.lean b/src/data/finmap.lean
@@ -8,6 +8,9 @@ import data.finset.basic
 import data.part
 /-!
 # Finite maps over `multiset`
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 universes u v w
diff --git a/src/data/finsupp/multiset.lean b/src/data/finsupp/multiset.lean
@@ -9,6 +9,9 @@ import data.finsupp.order
 /-!
 # Equivalence between `multiset` and `ℕ`-valued finitely supported functions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This defines `finsupp.to_multiset` the equivalence between `α →₀ ℕ` and `multiset α`, along
 with `multiset.to_finsupp` the reverse equivalence and `finsupp.order_iso_multiset` the equivalence
 promoted to an order isomorphism.
diff --git a/src/data/finsupp/to_dfinsupp.lean b/src/data/finsupp/to_dfinsupp.lean
@@ -10,6 +10,9 @@ import data.finsupp.basic
 /-!
 # Conversion between `finsupp` and homogenous `dfinsupp`
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This module provides conversions between `finsupp` and `dfinsupp`.
 It is in its own file since neither `finsupp` or `dfinsupp` depend on each other.
 
diff --git a/src/data/fp/basic.lean b/src/data/fp/basic.lean
@@ -7,6 +7,9 @@ import data.semiquot
 import data.rat.floor
 /-!
 # Implementation of floating-point numbers (experimental).
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 def int.shift2 (a b : ℕ) : ℤ → ℕ × ℕ
diff --git a/src/data/set_like/fintype.lean b/src/data/set_like/fintype.lean
@@ -8,6 +8,9 @@ import data.fintype.powerset
 /-!
 # Set-like fintype
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file contains a fintype instance for set-like objects such as subgroups. If `set_like A B`
 and `fintype B` then `fintype A`.
 -/
diff --git a/src/dynamics/fixed_points/topology.lean b/src/dynamics/fixed_points/topology.lean
@@ -9,6 +9,9 @@ import topology.separation
 /-!
 # Topological properties of fixed points
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Currently this file contains two lemmas:
 
 - `is_fixed_pt_of_tendsto_iterate`: if `f^n(x) → y` and `f` is continuous at `y`, then `f y = y`;
diff --git a/src/linear_algebra/general_linear_group.lean b/src/linear_algebra/general_linear_group.lean
@@ -8,6 +8,9 @@ import algebra.module.equiv
 /-!
 # The general linear group of linear maps
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The general linear group is defined to be the group of invertible linear maps from `M` to itself.
 
 See also `matrix.general_linear_group`
diff --git a/src/order/countable_dense_linear_order.lean b/src/order/countable_dense_linear_order.lean
@@ -9,6 +9,9 @@ import data.finset.lattice
 /-!
 # The back and forth method and countable dense linear orders
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Results
 
 Suppose `α β` are linear orders, with `α` countable and `β` dense, nontrivial. Then there is an
diff --git a/src/order/hom/lattice.lean b/src/order/hom/lattice.lean
@@ -10,6 +10,9 @@ import order.symm_diff
 /-!
 # Lattice homomorphisms
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines (bounded) lattice homomorphisms.
 
 We use the `fun_like` design, so each type of morphisms has a companion typeclass which is meant to
diff --git a/src/order/succ_pred/linear_locally_finite.lean b/src/order/succ_pred/linear_locally_finite.lean
@@ -13,6 +13,9 @@ import logic.encodable.basic
 /-!
 # Linear locally finite orders
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We prove that a `linear_order` which is a `locally_finite_order` also verifies
 * `succ_order`
 * `pred_order`
diff --git a/src/topology/omega_complete_partial_order.lean b/src/topology/omega_complete_partial_order.lean
@@ -9,6 +9,9 @@ import order.omega_complete_partial_order
 /-!
 # Scott Topological Spaces
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A type of topological spaces whose notion
 of continuity is equivalent to continuity in ωCPOs.
 
diff --git a/src/topology/uniform_space/cauchy.lean b/src/topology/uniform_space/cauchy.lean
@@ -7,6 +7,9 @@ import topology.bases
 import topology.uniform_space.basic
 /-!
 # Theory of Cauchy filters in uniform spaces. Complete uniform spaces. Totally bounded subsets.
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 universes u v
 
diff --git a/src/topology/uniform_space/separation.lean b/src/topology/uniform_space/separation.lean
@@ -11,6 +11,9 @@ import topology.separation
 /-!
 # Hausdorff properties of uniform spaces. Separation quotient.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file studies uniform spaces whose underlying topological spaces are separated
 (also known as Hausdorff or T₂).
 This turns out to be equivalent to asking that the intersection of all entourages
