Mathlib v3 is deprecated. Go to Mathlib v4

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