Commit 2023-02-02 08:10 9102b25d

View on Github →

feat: port Topology.DenseEmbedding (#2003)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/DenseEmbedding.lean

added theorem Dense.denseEmbedding_val

added theorem DenseEmbedding.dense_image

added theorem DenseEmbedding.inj_iff

added theorem DenseEmbedding.mk'

added def DenseEmbedding.subtypeEmb

added theorem DenseEmbedding.to_embedding

added structure DenseEmbedding

added theorem DenseInducing.closure_image_mem_nhds

added theorem DenseInducing.closure_range

added theorem DenseInducing.comap_nhds_neBot

added theorem DenseInducing.continuousAt_extend

added theorem DenseInducing.continuous_extend

added theorem DenseInducing.dense_image

added def DenseInducing.extend

added theorem DenseInducing.extend_eq'

added theorem DenseInducing.extend_eq

added theorem DenseInducing.extend_eq_at'

added theorem DenseInducing.extend_eq_at

added theorem DenseInducing.extend_eq_of_tendsto

added theorem DenseInducing.extend_unique

added theorem DenseInducing.extend_unique_at

added theorem DenseInducing.interior_compact_eq_empty

added theorem DenseInducing.mk'

added theorem DenseInducing.nhds_eq_comap

added theorem DenseInducing.tendsto_comap_nhds_nhds

added structure DenseInducing

added theorem DenseRange.equalizer

added theorem DenseRange.induction_on

added theorem DenseRange.induction_on₂

added theorem DenseRange.induction_on₃

added theorem Filter.HasBasis.hasBasis_of_denseInducing

added theorem denseEmbedding_id

added theorem isClosed_property2

added theorem isClosed_property3

added theorem isClosed_property