Zulip Chat Archive
Stream: mathlib4
Topic: Topology.MetricSpace.Closeds !4#3338
Moritz Firsching (Apr 08 2023 at 09:51):
In porting Topology.MetricSpace.Closeds, !4#3338, the only this left is a timeout in
lipschitz_infDist, help in fixing this would be appreciated!
Last updated: May 02 2025 at 03:31 UTC