Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-31 08:44 6a68f86a

View on Github →

chore(topology/algebra/order/basic): deduplicate (#16287) Primed and non-primed versions of 2 lemmas were almost defeq. Merge them.

Estimated changes