Commit 2025-03-19 19:40 1a55629d
View on Github →feat: covering a relatively compact set by balls (#23108) We already have the result for compact sets, but the relatively compact set is strictly harder (it requires the metric space characterisation of closure). From my PhD (MiscYD)