Theorem Metric.PiNatEmbed.ofPiNat_inj

Modification history

2025-12-17 21:56
Mathlib/Topology/MetricSpace/PiNat.lean
chore(Topology): fix whitespace (#32963) …
Modified Metric.PiNatEmbed.ofPiNat_injView on Github →
2025-11-04 14:52
Mathlib/Topology/MetricSpace/PiNat.lean
feat(Topology): embedding a countably separated space inside a space of sequences (#30849)
Added Metric.PiNatEmbed.ofPiNat_injView on Github →