Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-10-15 13:39 af434b54

View on Github →

refactor(analysis/topology): move is_open_map to continuity

Estimated changes

Modified analysis/topology/continuity.lean

added theorem is_open_map.of_inverse

added theorem is_open_map.to_quotient_map

added def is_open_map

added theorem is_open_map_iff_nhds_le

deleted theorem quotient_map.continuous

deleted theorem quotient_map.continuous_iff

deleted theorem quotient_map_compose

deleted theorem quotient_map_id

deleted theorem quotient_map_of_quotient_map_compose

Modified analysis/topology/quotient_topological_structures.lean

deleted theorem is_open_coinduced

deleted theorem is_open_map.of_inverse

deleted theorem is_open_map.to_quotient_map

deleted def is_open_map

deleted theorem is_open_map_iff_nhds_le

Modified analysis/topology/topological_space.lean

added theorem is_open_coinduced

added theorem is_open_induced_iff