Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-22 15:16 4c6b0de0

View on Github →

feat(topology/bases): disjoint unions of second-countable spaces are second-countable (#12061)

Estimated changes

Modified src/topology/bases.lean

added theorem is_topological_basis_singletons

added theorem topological_space.is_topological_basis.is_open_iff

added theorem topological_space.is_topological_basis.sigma

added theorem topological_space.is_topological_basis.sum

Modified src/topology/constructions.lean

added theorem closed_embedding_inl

added theorem closed_embedding_inr

added theorem is_closed_range_inl

added theorem is_closed_range_inr

Modified src/topology/continuous_on.lean

added theorem continuous_on.mono_dom

added theorem continuous_on.mono_rng

Modified src/topology/homeomorph.lean

added def equiv.to_homeomorph_of_inducing

Modified src/topology/order.lean

added theorem continuous_id_of_le