Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-02 20:02 78e50d8f

View on Github →

feat(order/topology/filter): define topology on filter X (#17219)

Estimated changes

added theorem continuous.nhds
added theorem continuous_at.nhds
added theorem continuous_on.nhds
added theorem filter.Inter_nhds
added theorem filter.continuous_nhds
added theorem filter.has_basis.nhds'
added theorem filter.has_basis.nhds
added theorem filter.inducing_nhds
added theorem filter.is_open_iff
added theorem filter.mem_nhds_iff'
added theorem filter.mem_nhds_iff
added theorem filter.monotone_nhds
added theorem filter.nhds_at_bot
added theorem filter.nhds_at_top
added theorem filter.nhds_bot
added theorem filter.nhds_eq'
added theorem filter.nhds_eq
added theorem filter.nhds_inf
added theorem filter.nhds_infi
added theorem filter.nhds_mono
added theorem filter.nhds_nhds
added theorem filter.nhds_principal
added theorem filter.nhds_pure
added theorem filter.nhds_top