P Paturi (May 22 2023 at 10:35): P Paturi (May 22 2023 at 10:35):Hi! Is there an already existing theory for metrci spaces in isabelle, extending the existing Topology theory? I haven't been able to find one in the archive of formal proofs.
Christian Pardillo Laursen (May 25 2023 at 13:33):Metric spaces are defined in Real_Vector_Spaces.thy, available as part of the standard library. Most of the theory for them is in HOL-Analysis
Last updated: Dec 21 2024 at 16:20 UTC