mathlib3
4355d171 - chore(topology/order): drop an unneeded argument (#6345)

Commit

4 years ago

chore(topology/order): drop an unneeded argument (#6345) `closure_induced` doesn't need `f` to be injective.

Author

urkud

Parents