Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-02-06 06:28 0a0ec350

View on Github →

chore(*): add mathlib4 synchronization comments (#18387) Regenerated from the port status wiki page. 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

Estimated changes