Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-11 04:32 4d27ecf7

View on Github →

refactor(order/conditionally_complete_lattice): csupr_le_csupr → csupr_mono (#13320) For consistency with supr_mono and infi_mono

Estimated changes

Modified src/dynamics/circle/rotation_number/translation_number.lean

Modified src/order/conditionally_complete_lattice.lean

deleted theorem cinfi_le_cinfi

added theorem cinfi_mono

deleted theorem csupr_le_csupr

added theorem csupr_mono

Modified src/topology/metric_space/gluing.lean

Modified src/topology/metric_space/gromov_hausdorff_realized.lean