Theorem PiCountable.edist_le_edist_pi_of_edist_lt

Modification history

2025-11-03 12:38
Mathlib/Topology/MetricSpace/PiNat.lean
feat(Topology): countable product of extended metric spaces (#30822) …
Added PiCountable.edist_le_edist_pi_of_edist_ltView on Github →