Commit 2025-11-04 14:52 d063ad5f

View on Github →

feat(Topology): embedding a countably separated space inside a space of sequences (#30849)

Estimated changes

Modified Mathlib/Topology/MetricSpace/PiNat.lean

added theorem Metric.PiNatEmbed.TopologicalSpace.MetrizableSpace.of_countable_separating

added theorem Metric.PiNatEmbed.continuous_toPiNat

added theorem Metric.PiNatEmbed.dist_def

added theorem Metric.PiNatEmbed.edist_def

added theorem Metric.PiNatEmbed.embed_injective

added theorem Metric.PiNatEmbed.ext

added theorem Metric.PiNatEmbed.isHomeomorph_toPiNat

added theorem Metric.PiNatEmbed.isUniformEmbedding_embed

added theorem Metric.PiNatEmbed.isometry_embed

added theorem Metric.PiNatEmbed.ofPiNat_inj

added def Metric.PiNatEmbed.toPiNatEquiv

added theorem Metric.PiNatEmbed.«forall»

added structure Metric.PiNatEmbed