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

Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following files: * `algebra.category.Group.epi_mono` * `algebra.category.Group.equivalence_Group_AddGroup` * `algebra.continued_fractions.computation.correctness_terminating` * `analysis.convex.partition_of_unity` * `analysis.normed.group.controlled_closure` * `analysis.normed_space.compact_operator` * `category_theory.abelian.pseudoelements` * `category_theory.preadditive.hom_orthogonal` * `category_theory.sites.cover_preserving` * `computability.halting` * `computability.partrec_code` * `dynamics.ergodic.ergodic` * `dynamics.ergodic.measure_preserving` * `measure_theory.covering.vitali_family` * `measure_theory.decomposition.unsigned_hahn` * `measure_theory.group.arithmetic` * `measure_theory.lattice` * `measure_theory.measure.mutually_singular` * `measure_theory.measure.open_pos` * `probability.conditional_probability` * `topology.algebra.equicontinuity` * `topology.category.Profinite.as_limit` * `topology.category.Top.limits.products` * `topology.continuous_function.locally_constant`
leanprover-community · May 11, 2023 · 781cb2e · 781cb2e
1 parent 5dc275e
commit 781cb2e
Show file tree

Hide file tree

Showing 24 changed files with 72 additions and 0 deletions.
diff --git a/src/algebra/category/Group/epi_mono.lean b/src/algebra/category/Group/epi_mono.lean
@@ -8,6 +8,9 @@ import group_theory.quotient_group
 
 /-!
 # Monomorphisms and epimorphisms in `Group`
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 In this file, we prove monomorphisms in category of group are injective homomorphisms and
 epimorphisms are surjective homomorphisms.
 -/

diff --git a/src/algebra/category/Group/equivalence_Group_AddGroup.lean b/src/algebra/category/Group/equivalence_Group_AddGroup.lean
@@ -9,6 +9,9 @@ import algebra.hom.equiv.type_tags
 /-!
 # Equivalence between `Group` and `AddGroup`
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file contains two equivalences:
 * `Group_AddGroup_equivalence` : the equivalence between `Group` and `AddGroup` by sending
   `X : Group` to `additive X` and `Y : AddGroup` to `multiplicative Y`.

diff --git a/src/algebra/continued_fractions/computation/correctness_terminating.lean b/src/algebra/continued_fractions/computation/correctness_terminating.lean
@@ -12,6 +12,9 @@ import tactic.field_simp
 /-!
 # Correctness of Terminating Continued Fraction Computations (`generalized_continued_fraction.of`)
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Summary
 
 We show the correctness of the

diff --git a/src/analysis/convex/partition_of_unity.lean b/src/analysis/convex/partition_of_unity.lean
@@ -9,6 +9,9 @@ import analysis.convex.combination
 /-!
 # Partition of unity and convex sets
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we prove the following lemma, see `exists_continuous_forall_mem_convex_of_local`. Let
 `X` be a normal paracompact topological space (e.g., any extended metric space). Let `E` be a
 topological real vector space. Let `t : X → set E` be a family of convex sets. Suppose that for each

diff --git a/src/analysis/normed/group/controlled_closure.lean b/src/analysis/normed/group/controlled_closure.lean
@@ -8,6 +8,9 @@ import analysis.specific_limits.normed
 
 /-! # Extending a backward bound on a normed group homomorphism from a dense set
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Possible TODO (from the PR's review, https://github.com/leanprover-community/mathlib/pull/8498 ):
 "This feels a lot like the second step in the proof of the Banach open mapping theorem
 (`exists_preimage_norm_le`) ... wonder if it would be possible to refactor it using one of [the

diff --git a/src/analysis/normed_space/compact_operator.lean b/src/analysis/normed_space/compact_operator.lean
@@ -9,6 +9,9 @@ import topology.algebra.module.strong_topology
 /-!
 # Compact operators
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define compact linear operators between two topological vector spaces (TVS).
 
 ## Main definitions

diff --git a/src/category_theory/abelian/pseudoelements.lean b/src/category_theory/abelian/pseudoelements.lean
@@ -10,6 +10,9 @@ import algebra.category.Module.epi_mono
 /-!
 # Pseudoelements in abelian categories
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A *pseudoelement* of an object `X` in an abelian category `C` is an equivalence class of arrows
 ending in `X`, where two arrows are considered equivalent if we can find two epimorphisms with a
 common domain making a commutative square with the two arrows. While the construction shows that

diff --git a/src/category_theory/preadditive/hom_orthogonal.lean b/src/category_theory/preadditive/hom_orthogonal.lean
@@ -10,6 +10,9 @@ import linear_algebra.matrix.invariant_basis_number
 /-!
 # Hom orthogonal families.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A family of objects in a category with zero morphisms is "hom orthogonal" if the only
 morphism between distinct objects is the zero morphism.
 

diff --git a/src/category_theory/sites/cover_preserving.lean b/src/category_theory/sites/cover_preserving.lean
@@ -10,6 +10,9 @@ import tactic.apply_fun
 /-!
 # Cover-preserving functors between sites.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We define cover-preserving functors between sites as functors that push covering sieves to
 covering sieves. A cover-preserving and compatible-preserving functor `G : C ⥤ D` then pulls
 sheaves on `D` back to sheaves on `C` via `G.op ⋙ -`.

diff --git a/src/computability/halting.lean b/src/computability/halting.lean
@@ -8,6 +8,9 @@ import computability.partrec_code
 /-!
 # Computability theory and the halting problem
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A universal partial recursive function, Rice's theorem, and the halting problem.
 
 ## References

diff --git a/src/computability/partrec_code.lean b/src/computability/partrec_code.lean
@@ -8,6 +8,9 @@ import computability.partrec
 /-!
 # Gödel Numbering for Partial Recursive Functions.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines `nat.partrec.code`, an inductive datatype describing code for partial
 recursive functions on ℕ. It defines an encoding for these codes, and proves that the constructors
 are primitive recursive with respect to the encoding.

diff --git a/src/dynamics/ergodic/ergodic.lean b/src/dynamics/ergodic/ergodic.lean
@@ -8,6 +8,9 @@ import dynamics.ergodic.measure_preserving
 /-!
 # Ergodic maps and measures
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Let `f : α → α` be measure preserving with respect to a measure `μ`. We say `f` is ergodic with
 respect to `μ` (or `μ` is ergodic with respect to `f`) if the only measurable sets `s` such that
 `f⁻¹' s = s` are either almost empty or full.

diff --git a/src/dynamics/ergodic/measure_preserving.lean b/src/dynamics/ergodic/measure_preserving.lean
@@ -8,6 +8,9 @@ import measure_theory.measure.ae_measurable
 /-!
 # Measure preserving maps
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We say that `f : α → β` is a measure preserving map w.r.t. measures `μ : measure α` and
 `ν : measure β` if `f` is measurable and `map f μ = ν`. In this file we define the predicate
 `measure_theory.measure_preserving` and prove its basic properties.

diff --git a/src/measure_theory/covering/vitali_family.lean b/src/measure_theory/covering/vitali_family.lean
@@ -8,6 +8,9 @@ import measure_theory.measure.measure_space
 /-!
 # Vitali families
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 On a metric space `X` with a measure `μ`, consider for each `x : X` a family of measurable sets with
 nonempty interiors, called `sets_at x`. This family is a Vitali family if it satisfies the following
 property: consider a (possibly non-measurable) set `s`, and for any `x` in `s` a

diff --git a/src/measure_theory/decomposition/unsigned_hahn.lean b/src/measure_theory/decomposition/unsigned_hahn.lean
@@ -8,6 +8,9 @@ import measure_theory.measure.measure_space
 /-!
 # Unsigned Hahn decomposition theorem
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file proves the unsigned version of the Hahn decomposition theorem.
 
 ## Main statements

diff --git a/src/measure_theory/group/arithmetic.lean b/src/measure_theory/group/arithmetic.lean
@@ -8,6 +8,9 @@ import measure_theory.measure.ae_measurable
 /-!
 # Typeclasses for measurability of operations
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define classes `has_measurable_mul` etc and prove dot-style lemmas
 (`measurable.mul`, `ae_measurable.mul` etc). For binary operations we define two typeclasses:
 

diff --git a/src/measure_theory/lattice.lean b/src/measure_theory/lattice.lean
@@ -9,6 +9,9 @@ import measure_theory.measure.ae_measurable
 /-!
 # Typeclasses for measurability of lattice operations
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define classes `has_measurable_sup` and `has_measurable_inf` and prove dot-style
 lemmas (`measurable.sup`, `ae_measurable.sup` etc). For binary operations we define two typeclasses:
 

diff --git a/src/measure_theory/measure/mutually_singular.lean b/src/measure_theory/measure/mutually_singular.lean
@@ -7,6 +7,9 @@ import measure_theory.measure.measure_space
 
 /-! # Mutually singular measures
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Two measures `μ`, `ν` are said to be mutually singular (`measure_theory.measure.mutually_singular`,
 localized notation `μ ⟂ₘ ν`) if there exists a measurable set `s` such that `μ s = 0` and
 `ν sᶜ = 0`. The measurability of `s` is an unnecessary assumption (see

diff --git a/src/measure_theory/measure/open_pos.lean b/src/measure_theory/measure/open_pos.lean
@@ -8,6 +8,9 @@ import measure_theory.measure.measure_space
 /-!
 # Measures positive on nonempty opens
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define a typeclass for measures that are positive on nonempty opens, see
 `measure_theory.measure.is_open_pos_measure`. Examples include (additive) Haar measures, as well as
 measures that have positive density with respect to a Haar measure. We also prove some basic facts

diff --git a/src/probability/conditional_probability.lean b/src/probability/conditional_probability.lean
@@ -8,6 +8,9 @@ import measure_theory.measure.measure_space
 /-!
 # Conditional Probability
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines conditional probability and includes basic results relating to it.
 
 Given some measure `μ` defined on a measure space on some type `Ω` and some `s : set Ω`,

diff --git a/src/topology/algebra/equicontinuity.lean b/src/topology/algebra/equicontinuity.lean
@@ -7,6 +7,9 @@ import topology.algebra.uniform_convergence
 
 /-!
 # Algebra-related equicontinuity criterions
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 open function

diff --git a/src/topology/category/Profinite/as_limit.lean b/src/topology/category/Profinite/as_limit.lean
@@ -9,6 +9,9 @@ import topology.discrete_quotient
 /-!
 # Profinite sets as limits of finite sets.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We show that any profinite set is isomorphic to the limit of its
 discrete (hence finite) quotients.
 

diff --git a/src/topology/category/Top/limits/products.lean b/src/topology/category/Top/limits/products.lean
@@ -9,6 +9,9 @@ import topology.category.Top.limits.basic
 /-!
 # Products and coproducts in the category of topological spaces
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 -/
 
 open topological_space

diff --git a/src/topology/continuous_function/locally_constant.lean b/src/topology/continuous_function/locally_constant.lean
@@ -10,6 +10,9 @@ import topology.continuous_function.algebra
 /-!
 # The algebra morphism from locally constant functions to continuous functions.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 -/
 
 namespace locally_constant