Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-18 13:26 b352d2cb

View on Github →

refactor(topology): topological_space.induced resembles set.image; second_countable_topology on subtypes; simplify filter.map_comap

Estimated changes

Modified src/order/filter.lean

deleted theorem filter.le_map_comap'

deleted theorem filter.le_map_comap

added theorem filter.map_comap

deleted theorem filter.tendsto_comap''

added theorem filter.tendsto_comap'_iff

Modified src/topology/basic.lean

added theorem induced_generate_from_eq

added theorem topological_space.second_countable_topology_induced

Modified src/topology/continuity.lean

modified theorem embedding.map_nhds_eq

added theorem is_open_induced_eq

modified theorem map_nhds_induced_eq

Modified src/topology/instances/ennreal.lean

deleted theorem ennreal.coe_image_univ_mem_nhds

added theorem ennreal.coe_range_mem_nhds

Modified src/topology/instances/nnreal.lean

Modified src/topology/uniform_space/basic.lean

Modified src/topology/uniform_space/completion.lean