Mathlib Changelog
Changelog
About
Github
Commit
2022-09-20 05:26
0a67ddd4
View on Github →
feat(topology/separation): define
regular_space
(
#16360
)
Estimated changes
Modified
src/analysis/locally_convex/balanced_core_hull.lean
modified
theorem
nhds_basis_closed_balanced
Modified
src/order/filter/bases.lean
added
theorem
filter.has_basis.disjoint_iff_left
added
theorem
filter.has_basis.disjoint_iff_right
Modified
src/topology/algebra/group.lean
modified
theorem
topological_group.t3_space
Modified
src/topology/algebra/infinite_sum.lean
modified
theorem
has_sum.prod_fiberwise
modified
theorem
has_sum.sigma
modified
theorem
summable.sigma'
modified
theorem
summable.sigma
modified
theorem
tendsto_tsum_compl_at_top_zero
modified
theorem
tsum_comm'
modified
theorem
tsum_prod'
modified
theorem
tsum_sigma'
Modified
src/topology/algebra/order/basic.lean
Modified
src/topology/algebra/order/extend_from.lean
Modified
src/topology/algebra/with_zero_topology.lean
Modified
src/topology/dense_embedding.lean
Modified
src/topology/extend_from.lean
modified
theorem
continuous_extend_from
modified
theorem
continuous_on_extend_from
Modified
src/topology/inseparable.lean
added
theorem
filter.has_basis.specializes_iff
Modified
src/topology/order.lean
added
theorem
is_closed.mono
added
theorem
is_open.mono
Modified
src/topology/separation.lean
modified
theorem
closed_nhds_basis
added
theorem
disjoint_nhds_nhds_iff_not_specializes
added
theorem
disjoint_nhds_nhds_set
added
theorem
disjoint_nhds_set_nhds
added
theorem
exists_mem_nhds_is_closed_subset
added
theorem
filter.has_basis.nhds_closure
added
theorem
has_basis_nhds_closure
added
theorem
has_basis_opens_closure
added
theorem
is_closed_set_of_inseparable
added
theorem
is_closed_set_of_specializes
added
theorem
is_open_set_of_disjoint_nhds_nhds
added
theorem
lift'_nhds_closure
deleted
theorem
nhds_is_closed
added
theorem
regular_space.inf
added
theorem
regular_space.of_basis
added
theorem
regular_space.of_exists_mem_nhds_is_closed_subset
added
theorem
regular_space.of_lift'_closure
added
theorem
regular_space_Inf
added
theorem
regular_space_induced
added
theorem
regular_space_infi
added
theorem
regular_space_tfae
added
theorem
specializes_comm
added
theorem
specializes_iff_inseparable
deleted
theorem
t3_space.of_lift'_closure
modified
theorem
topological_space.is_topological_basis.exists_closure_subset
modified
theorem
topological_space.is_topological_basis.nhds_basis_closure
Modified
src/topology/uniform_space/separation.lean