Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-20 21:10 93d17601

View on Github →

chore(topology/bases): golf a proof (#6326) Also add some supporting lemmas

Estimated changes

Modified src/topology/bases.lean

added theorem topological_space.is_topological_basis.dense_iff

added theorem topological_space.is_topological_basis.mem_closure_iff

Modified src/topology/basic.lean

added theorem filter.has_basis.cluster_pt_iff

added theorem mem_closure_iff_nhds_basis'