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

Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following files: * `algebra.graded_mul_action` * `category_theory.sigma.basic` * `combinatorics.set_family.intersecting` * `combinatorics.set_family.lym` * `data.finsupp.alist` * `data.pfun` * `group_theory.presented_group` * `group_theory.quotient_group` * `group_theory.submonoid.inverses` * `order.ideal` * `set_theory.lists` * `topology.algebra.const_mul_action` * `topology.algebra.constructions` * `topology.connected` * `topology.dense_embedding` * `topology.homeomorph` * `topology.separation` * `topology.support` * `topology.uniform_space.basic`
leanprover-community · Feb 3, 2023 · 0ebfdb7 · 0ebfdb7
1 parent 84dc0bd
commit 0ebfdb7
Show file tree

Hide file tree

Showing 19 changed files with 57 additions and 0 deletions.
diff --git a/src/algebra/graded_mul_action.lean b/src/algebra/graded_mul_action.lean
@@ -8,6 +8,9 @@ import algebra.graded_monoid
 /-!
 # Additively-graded multiplicative action structures
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This module provides a set of heterogeneous typeclasses for defining a multiplicative structure
 over the sigma type `graded_monoid A` such that `(•) : A i → M j → M (i + j)`; that is to say, `A`
 has an additively-graded multiplicative action on `M`. The typeclasses are:

diff --git a/src/category_theory/sigma/basic.lean b/src/category_theory/sigma/basic.lean
@@ -10,6 +10,9 @@ import category_theory.natural_isomorphism
 /-!
 # Disjoint union of categories
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We define the category structure on a sigma-type (disjoint union) of categories.
 -/
 

diff --git a/src/combinatorics/set_family/intersecting.lean b/src/combinatorics/set_family/intersecting.lean
@@ -9,6 +9,9 @@ import order.upper_lower.basic
 /-!
 # Intersecting families
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines intersecting families and proves their basic properties.
 
 ## Main declarations

diff --git a/src/combinatorics/set_family/lym.lean b/src/combinatorics/set_family/lym.lean
@@ -12,6 +12,9 @@ import data.rat.order
 /-!
 # Lubell-Yamamoto-Meshalkin inequality and Sperner's theorem
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file proves the local LYM and LYM inequalities as well as Sperner's theorem.
 
 ## Main declarations

diff --git a/src/data/finsupp/alist.lean b/src/data/finsupp/alist.lean
@@ -9,6 +9,9 @@ import data.list.alist
 /-!
 # Connections between `finsupp` and `alist`
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Main definitions
 
 * `finsupp.to_alist`

diff --git a/src/data/pfun.lean b/src/data/pfun.lean
@@ -9,6 +9,9 @@ import data.rel
 /-!
 # Partial functions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines partial functions. Partial functions are like functions, except they can also be
 "undefined" on some inputs. We define them as functions `α → part β`.
 

diff --git a/src/group_theory/presented_group.lean b/src/group_theory/presented_group.lean
@@ -9,6 +9,9 @@ import group_theory.quotient_group
 /-!
 # Defining a group given by generators and relations
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Given a subset `rels` of relations of the free group on a type `α`, this file constructs the group
 given by generators `x : α` and relations `r ∈ rels`.
 

diff --git a/src/group_theory/quotient_group.lean b/src/group_theory/quotient_group.lean
@@ -13,6 +13,9 @@ import group_theory.subgroup.pointwise
 /-!
 # Quotients of groups by normal subgroups
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This files develops the basic theory of quotients of groups by normal subgroups. In particular it
 proves Noether's first and second isomorphism theorems.
 

diff --git a/src/group_theory/submonoid/inverses.lean b/src/group_theory/submonoid/inverses.lean
@@ -10,6 +10,9 @@ import group_theory.submonoid.pointwise
 
 # Submonoid of inverses
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Given a submonoid `N` of a monoid `M`, we define the submonoid `N.left_inv` as the submonoid of
 left inverses of `N`. When `M` is commutative, we may define `from_comm_left_inv : N.left_inv →* N`
 since the inverses are unique. When `N ≤ is_unit.submonoid M`, this is precisely

diff --git a/src/order/ideal.lean b/src/order/ideal.lean
@@ -10,6 +10,9 @@ import order.upper_lower.basic
 /-!
 # Order ideals, cofinal sets, and the Rasiowa–Sikorski lemma
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Main definitions
 
 Throughout this file, `P` is at least a preorder, but some sections require more

diff --git a/src/set_theory/lists.lean b/src/set_theory/lists.lean
@@ -8,6 +8,9 @@ import data.list.basic
 /-!
 # A computable model of ZFA without infinity
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define finite hereditary lists. This is useful for calculations in naive set theory.
 
 We distinguish two kinds of ZFA lists:

diff --git a/src/topology/algebra/const_mul_action.lean b/src/topology/algebra/const_mul_action.lean
@@ -12,6 +12,9 @@ import topology.support
 /-!
 # Monoid actions continuous in the second variable
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define class `has_continuous_const_smul`. We say `has_continuous_const_smul Γ T` if
 `Γ` acts on `T` and for each `γ`, the map `x ↦ γ • x` is continuous. (This differs from
 `has_continuous_smul`, which requires simultaneous continuity in both variables.)

diff --git a/src/topology/algebra/constructions.lean b/src/topology/algebra/constructions.lean
@@ -8,6 +8,9 @@ import topology.homeomorph
 /-!
 # Topological space structure on the opposite monoid and on the units group
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define `topological_space` structure on `Mᵐᵒᵖ`, `Mᵃᵒᵖ`, `Mˣ`, and `add_units M`.
 This file does not import definitions of a topological monoid and/or a continuous multiplicative
 action, so we postpone the proofs of `has_continuous_mul Mᵐᵒᵖ` etc till we have these definitions.

diff --git a/src/topology/connected.lean b/src/topology/connected.lean
@@ -11,6 +11,9 @@ import tactic.congrm
 /-!
 # Connected subsets of topological spaces
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define connected subsets of a topological spaces and various other properties and
 classes related to connectivity.
 

diff --git a/src/topology/dense_embedding.lean b/src/topology/dense_embedding.lean
@@ -9,6 +9,9 @@ import topology.bases
 /-!
 # Dense embeddings
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines three properties of functions:
 
 * `dense_range f`      means `f` has dense image;

diff --git a/src/topology/homeomorph.lean b/src/topology/homeomorph.lean
@@ -10,6 +10,9 @@ import topology.support
 /-!
 # Homeomorphisms
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines homeomorphisms between two topological spaces. They are bijections with both
 directions continuous. We denote homeomorphisms with the notation `≃ₜ`.
 

diff --git a/src/topology/separation.lean b/src/topology/separation.lean
@@ -11,6 +11,9 @@ import topology.inseparable
 /-!
 # Separation properties of topological spaces.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines the predicate `separated_nhds`, and common separation axioms
 (under the Kolmogorov classification).
 

diff --git a/src/topology/support.lean b/src/topology/support.lean
@@ -9,6 +9,9 @@ import topology.separation
 /-!
 # The topological support of a function
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define the topological support of a function `f`, `tsupport f`,
 as the closure of the support of `f`.
 

diff --git a/src/topology/uniform_space/basic.lean b/src/topology/uniform_space/basic.lean
@@ -10,6 +10,9 @@ import topology.nhds_set
 /-!
 # Uniform spaces
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Uniform spaces are a generalization of metric spaces and topological groups. Many concepts directly
 generalize to uniform spaces, e.g.