Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-09 23:56 660a6c49

View on Github →

feat(topology): misc topological lemmas (#4091) From the sphere eversion project.

Estimated changes

Modified src/order/filter/bases.lean

added theorem filter.is_countably_generated.inf

added theorem filter.is_countably_generated.inf_principal

added theorem filter.is_countably_generated_principal

Modified src/order/filter/basic.lean

added theorem filter.diff_mem_inf_principal_compl

Modified src/topology/bases.lean

added def topological_space.dense_seq

added theorem topological_space.dense_seq_dense

added theorem topological_space.exists_dense_seq

added theorem topological_space.is_countably_generated_nhds

added theorem topological_space.is_countably_generated_nhds_within

Modified src/topology/continuous_on.lean

added theorem diff_mem_nhds_within_compl