Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-10-19 00:03 f6812d5a

View on Github →

feat(analysis/topology): add type class for discrete topological spaces

Estimated changes

Modified analysis/topology/continuity.lean

Modified analysis/topology/topological_space.lean

added theorem is_open_discrete

deleted theorem is_open_top

added theorem nhds_discrete

added theorem nhds_top

deleted theorem t2_space_top

added theorem tendsto_pure_nhds

Modified order/filter.lean

added theorem filter.map_prod

added theorem filter.mem_map_seq_iff

added theorem filter.mem_pure_iff

added theorem filter.prod_eq

added theorem filter.tendsto_const_pure

added theorem filter.tendsto_pure_pure