Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-03-12 00:23 c985ae98

View on Github →

chore(topology/order/basic): generalise frontier_Icc (#18571)

Estimated changes

modified theorem frontier_Icc