Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-06 12:20 0e533d06

View on Github →

refactor(topology/basic): rewrite some proofs using filter bases (#1967)

Estimated changes

Modified src/topology/basic.lean

added theorem mem_closure_iff_nhds_basis

added theorem nhds_basis_opens

deleted theorem nhds_sets

Modified src/topology/bounded_continuous_function.lean

Modified src/topology/order.lean