Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-13 02:53 14749964

View on Github →

feat(topology/basic): add nhds_basis_closeds (#14083)

  • add nhds_basis_closeds;
  • golf 2 proofs;
  • move topological_space.seq_tendsto_iff to topology.basic, rename it to tendsto_at_top_nhds.

Estimated changes

added theorem nhds_basis_closeds
modified theorem nhds_basis_opens
added theorem tendsto_at_top_nhds