Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-25 21:29 1a526b31

View on Github →

chore(topology/homeomorph): a few more lemmas, golf (#5467)

Estimated changes

Modified src/topology/homeomorph.lean

modified theorem homeomorph.coinduced_eq

added theorem homeomorph.comap_nhds_eq

added theorem homeomorph.image_closure

added theorem homeomorph.image_preimage

modified theorem homeomorph.induced_eq

added theorem homeomorph.is_closed_image

added theorem homeomorph.is_closed_preimage

added theorem homeomorph.is_open_image

added theorem homeomorph.map_nhds_eq

added theorem homeomorph.nhds_eq_comap

added theorem homeomorph.preimage_closure

added theorem homeomorph.preimage_image

Modified src/topology/maps.lean