Commit 2023-06-23 06:08 fcb2f0f3

View on Github →

remove conditional completeness assumption in IsCompact.exists_isMinOn (#5388) Also rename 2 lemmas

IsCompact.exists_local_min_mem_open -> IsCompact.exists_isLocalMin_mem_open;
Metric.exists_local_min_mem_ball -> Metric.exists_isLocal_min_mem_ball.

Estimated changes

Modified Mathlib/Analysis/Complex/OpenMapping.lean

Modified Mathlib/Order/Directed.lean

added theorem IsTotal.directed

Modified Mathlib/Topology/Algebra/Order/Compact.lean

added theorem Continuous.bddAbove_range_of_hasCompactMulSupport

added theorem Continuous.bddBelow_range_of_hasCompactMulSupport

added theorem IsCompact.bddAbove

added theorem IsCompact.bddAbove_image

added theorem IsCompact.bddBelow

added theorem IsCompact.bddBelow_image

added theorem IsCompact.exists_isLocalMin_mem_open

deleted theorem IsCompact.exists_local_min_mem_open

Modified Mathlib/Topology/MetricSpace/Basic.lean

added theorem Metric.exists_isLocalMin_mem_ball

deleted theorem Metric.exists_local_min_mem_ball

Modified Mathlib/Topology/Order/Basic.lean

deleted theorem Continuous.bddAbove_range_of_hasCompactMulSupport

deleted theorem Continuous.bddBelow_range_of_hasCompactMulSupport

deleted theorem IsCompact.bddAbove

deleted theorem IsCompact.bddAbove_image

deleted theorem IsCompact.bddBelow

deleted theorem IsCompact.bddBelow_image

Modified Mathlib/Topology/SubsetProperties.lean

added theorem IsCompact.elim_directed_family_closed