Theorem Metric.exists_isLocalMin_mem_ball

Modification history

2024-07-15 21:27
Mathlib/Topology/MetricSpace/ProperSpace.lean
chore: split some lemmas out of Topology.MetricSpace.ProperSpace (#13834) …
Modified Metric.exists_isLocalMin_mem_ballView on Github →
2024-01-18 02:11
Mathlib/Topology/MetricSpace/ProperSpace.lean
chore(MetricSpace/PseudoMetric): split out proper spaces (#9812) …
Modified Metric.exists_isLocalMin_mem_ballView on Github →
2023-10-30 10:24
Mathlib/Topology/MetricSpace/Basic.lean
chore: split MetricSpace.basic (#7920) …
Modified Metric.exists_isLocalMin_mem_ballView on Github →
2023-06-23 06:08
Mathlib/Topology/MetricSpace/Basic.lean
remove conditional completeness assumption in `IsCompact.exists_isMinOn` (#5388) …
Added Metric.exists_isLocalMin_mem_ballView on Github →