Mathlib Changelog
v3
Changelog
About
Github
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
Modified
src/data/set/basic.lean
added
theorem
set.exists_subset_range_and_iff
added
theorem
set.exists_subset_range_iff
Created
src/topology/algebra/order/filter.lean
added
theorem
filter.tendsto.nhds_at_bot
added
theorem
filter.tendsto.nhds_at_top
Modified
src/topology/bases.lean
added
theorem
topological_space.is_topological_basis.open_iff_eq_sUnion
Created
src/topology/filter.lean
added
theorem
continuous.nhds
added
theorem
continuous_at.nhds
added
theorem
continuous_on.nhds
added
theorem
continuous_within_at.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_Iic_principal
added
theorem
filter.is_open_iff
added
theorem
filter.is_open_set_of_mem
added
theorem
filter.is_topological_basis_Iic_principal
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
added
theorem
filter.specializes_iff_le