Email Gateway (May 01 2025 at 14:44): Email Gateway (May 01 2025 at 14:44):From: Lawrence Paulson <lp15@cam.ac.uk>
I'm happy to announce a new contribution:
Definition and Elementary Properties of Ultrametric Spaces
Benoît Ballenghien , Benjamin Puyobro and Burkhart Wolff
An ultrametric space is a metric space in which the triangle inequality is strengthened by using the maximum instead of the sum. … In this entry, we present an elementary formalization of these spaces relying on axiomatic type classes. The connection with standard metric spaces is obtained through a subclass relationship, and fundamental properties of ultrametric spaces are formally established.
https://www.isa-afp.org/entries/Elementary_Ultrametric_Spaces.html
Larry
Last updated: May 06 2025 at 08:28 UTC