Commit 2024-06-14 08:24 294e3c6e

View on Github →

chore: remove some of the >1year deprecations (#13792)

Estimated changes

Modified Mathlib/Data/List/Chain.lean

deleted theorem List.chain'_iff_nthLe

deleted theorem List.chain_iff_nthLe

Modified Mathlib/Data/List/Cycle.lean

Modified Mathlib/Order/Filter/Pointwise.lean

Modified Mathlib/Topology/MetricSpace/PseudoMetric.lean

Modified Mathlib/Topology/Order/Basic.lean

deleted theorem countable_of_isolated_right'

Modified Mathlib/Topology/Order/LeftRightNhds.lean

deleted theorem Filter.map_neg_eq_comap_neg

deleted theorem preimage_neg

Modified Mathlib/Topology/Order/ProjIcc.lean

deleted theorem Filter.Tendsto.IccExtend'

Modified Mathlib/Topology/Separation.lean

deleted theorem TopologicalSpace.subset_trans

Modified scripts/noshake.json