Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-02 06:43 541b2880

View on Github →

chore(topology/order): open function, don't open classical (#16288)

Estimated changes

modified theorem set_of_is_open_injective