Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-01-06 23:48 a1b73125

View on Github →

feat(topology/maps): a few lemmas about is_open_map (#1855)

feat(topology/maps): a few lemmas about is_open_map Also fix arguments order in all *.comp in this file.
Use restricted version of continuous_of_left_inverse to prove non-restricted
Fix compile by reverting a name change

Estimated changes

Modified src/topology/constructions.lean

added theorem is_closed.closed_embedding_subtype_val

added theorem is_open.is_open_map_subtype_val

added theorem is_open.open_embedding_subtype_val

added theorem is_open_map.restrict

deleted theorem subtype_val.closed_embedding

deleted theorem subtype_val.open_embedding

Modified src/topology/continuous_on.lean

added theorem is_open_map.continuous_on_image_of_left_inv_on

added theorem is_open_map.continuous_on_range_of_left_inverse

Modified src/topology/maps.lean

modified theorem closed_embedding.comp

modified theorem embedding.comp

deleted theorem inducing.comp

added theorem is_open_map.is_open_range

added theorem is_open_map.nhds_le

modified theorem is_open_map_iff_nhds_le

modified theorem open_embedding.comp

modified def quotient_map