Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-21 17:46 9a7a611c

View on Github →

feat(analysis/topology, order/filter): theorems for the applicative structure on filter; add list topology

Estimated changes

Modified analysis/topology/topological_space.lean

added theorem nhds_list

modified theorem quotient_dense_of_dense

added theorem topological_space.nhds_mk_of_nhds

Modified order/filter.lean

added theorem filter.comap_Sup

added theorem filter.comap_supr

added theorem filter.le_map

added theorem filter.le_seq

added theorem filter.map_pure

added theorem filter.mem_map_sets_iff

added theorem filter.mem_seq_sets_def

added theorem filter.mem_seq_sets_iff

added theorem filter.mem_traverse_sets

added theorem filter.mem_traverse_sets_iff

added theorem filter.prod_map_seq_comm

added theorem filter.pure_seq_eq_map

added theorem filter.seq_assoc

added theorem filter.seq_mem_seq_sets

modified theorem filter.seq_mono

added theorem filter.seq_pure

added theorem filter.sequence_mono

added theorem filter.singleton_mem_pure_sets

added theorem filter.{l}