Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-21 18:45 4355d171

View on Github →

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

Estimated changes

Modified src/topology/constructions.lean

Modified src/topology/maps.lean

added theorem inducing.closure_eq_preimage_closure_image

Modified src/topology/order.lean

modified theorem closure_induced

Modified src/topology/uniform_space/uniform_embedding.lean