Theorem Metric.PiNatEmbed.«forall»

Modification history

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.«forall»View on Github →