Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2019-10-07 21:52
1bf831f2
View on Github →
refactor(topology/dense_embedding): move dense embeddings to new file (
#1515
)
Estimated changes
Modified
src/topology/constructions.lean
Created
src/topology/dense_embedding.lean
added
theorem
dense_embedding.inj_iff
added
theorem
dense_embedding.mk'
added
theorem
dense_embedding.to_embedding
added
structure
dense_embedding
added
theorem
dense_inducing.closure_image_nhds_of_nhds
added
theorem
dense_inducing.closure_range
added
theorem
dense_inducing.comap_nhds_neq_bot
added
theorem
dense_inducing.continuous_extend
added
def
dense_inducing.extend
added
theorem
dense_inducing.extend_e_eq
added
theorem
dense_inducing.extend_eq
added
theorem
dense_inducing.extend_eq_of_cont
added
theorem
dense_inducing.mk'
added
theorem
dense_inducing.nhds_eq_comap
added
theorem
dense_inducing.self_sub_closure_image_preimage_of_open
added
theorem
dense_inducing.tendsto_comap_nhds_nhds
added
theorem
dense_inducing.tendsto_extend
added
structure
dense_inducing
added
theorem
dense_range.comp
added
def
dense_range.inhabited
added
theorem
dense_range.nonempty
added
def
dense_range
added
theorem
dense_range_iff_closure_eq
Modified
src/topology/maps.lean
deleted
theorem
dense_embedding.inj_iff
deleted
theorem
dense_embedding.mk'
deleted
theorem
dense_embedding.to_embedding
deleted
structure
dense_embedding
deleted
theorem
dense_inducing.closure_image_nhds_of_nhds
deleted
theorem
dense_inducing.closure_range
deleted
theorem
dense_inducing.comap_nhds_neq_bot
deleted
theorem
dense_inducing.continuous_extend
deleted
def
dense_inducing.extend
deleted
theorem
dense_inducing.extend_e_eq
deleted
theorem
dense_inducing.extend_eq
deleted
theorem
dense_inducing.extend_eq_of_cont
deleted
theorem
dense_inducing.mk'
deleted
theorem
dense_inducing.nhds_eq_comap
deleted
theorem
dense_inducing.self_sub_closure_image_preimage_of_open
deleted
theorem
dense_inducing.tendsto_comap_nhds_nhds
deleted
theorem
dense_inducing.tendsto_extend
deleted
structure
dense_inducing
deleted
theorem
dense_range.comp
deleted
def
dense_range.inhabited
deleted
theorem
dense_range.nonempty
deleted
def
dense_range
deleted
theorem
dense_range_iff_closure_eq