α : Type u
β : Type v
X : Type ?u.542746
ι : Type ?u.542749
inst✝⁴ : PseudoMetricSpace α
inst✝³ : ProperSpace α
inst✝² : TopologicalSpace β
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a z : α
r : ℝ
hf : ContinuousOn f (closedBall a r)
hz : z ∈ closedBall a r
hf1 : ∀ (z' : α), z' ∈ closedBall a r \ ball a r → f z < f z'
⊢ ∃ z, z ∈ ball a r ∧ IsLocalMin f z
α : Type u
β : Type v
X : Type ?u.542746
ι : Type ?u.542749
inst✝⁴ : PseudoMetricSpace α
inst✝³ : ProperSpace α
inst✝² : TopologicalSpace β
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a z : α
r : ℝ
hf : ContinuousOn f (closedBall a r)
hz : z ∈ closedBall a r
hf1 : ∀ (z' : α), z' ∈ sphere a r → f z < f z'
⊢ ∃ z, z ∈ ball a r ∧ IsLocalMin f z
simp_rw [← closedBall_diff_ball] at hf1
no goals
α : Type u
β : Type v
X : Type ?u.542746
ι : Type ?u.542749
inst✝⁴ : PseudoMetricSpace α
inst✝³ : ProperSpace α
inst✝² : TopologicalSpace β
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a z : α
r : ℝ
hf : ContinuousOn f (closedBall a r)
hz : z ∈ closedBall a r
hf1 : ∀ (z' : α), z' ∈ closedBall a r \ ball a r → f z < f z'
⊢ ∃ z, z ∈ ball a r ∧ IsLocalMin f z
exact (isCompact_closedBall a r).exists_local_min_mem_open ball_subset_closedBall hf hz hf1
  isOpen_ball