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: Dec 20 2023 at 11:08 UTC