Theorem exists_pos_lt_subset_ball

Modification history

2024-07-15 21:27
Mathlib/Topology/MetricSpace/ProperSpace.lean
chore: split some lemmas out of Topology.MetricSpace.ProperSpace (#13834) …
Modified exists_pos_lt_subset_ballView on Github →
2024-01-18 02:11
Mathlib/Topology/MetricSpace/ProperSpace.lean
chore(MetricSpace/PseudoMetric): split out proper spaces (#9812) …
Modified exists_pos_lt_subset_ballView on Github →
2023-10-30 10:24
Mathlib/Topology/MetricSpace/Basic.lean
chore: split MetricSpace.basic (#7920) …
Modified exists_pos_lt_subset_ballView on Github →
2023-03-03 17:48
Mathlib/Topology/MetricSpace/Basic.lean
feat: port Topology.MetricSpace.Basic (#2425)
Added exists_pos_lt_subset_ballView on Github →