E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure U)
⊢ ∃ z, z ∈ frontier U ∧ IsMaxOn (norm ∘ f) (closure U) z
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
⊢ ∃ z, z ∈ frontier U ∧ IsMaxOn (norm ∘ f) (closure U) z
have hc : IsCompact (closure U) := hb.isCompact_closure
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure U)
⊢ ∃ w, w ∈ closure U ∧ IsMaxOn (norm ∘ f) (closure U) w

case intro.intro
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure U)
w : E
hwU : w ∈ closure U
hle : IsMaxOn (norm ∘ f) (closure U) w
⊢ ∃ z, z ∈ frontier U ∧ IsMaxOn (norm ∘ f) (closure U) z
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure U)
⊢ ∃ z, z ∈ frontier U ∧ IsMaxOn (norm ∘ f) (closure U) z
obtain ⟨w, hwU, hle⟩ : ∃ w ∈ closure U, IsMaxOn (norm ∘ f) (closure U) w
case intro.intro
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure U)
w : E
hwU : w ∈ closure U
hle : IsMaxOn (norm ∘ f) (closure U) w
⊢ ∃ z, z ∈ frontier U ∧ IsMaxOn (norm ∘ f) (closure U) z
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure U)
⊢ ∃ w, w ∈ closure U ∧ IsMaxOn (norm ∘ f) (closure U) w

case intro.intro
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure U)
w : E
hwU : w ∈ closure U
hle : IsMaxOn (norm ∘ f) (closure U) w
⊢ ∃ z, z ∈ frontier U ∧ IsMaxOn (norm ∘ f) (closure U) z
exact hc.exists_forall_ge hne.closure hd.continuousOn.norm
case intro.intro
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure U)
w : E
hwU : w ∈ interior U ∨ w ∈ frontier U
hle : IsMaxOn (norm ∘ f) (closure U) w
⊢ ∃ z, z ∈ frontier U ∧ IsMaxOn (norm ∘ f) (closure U) z
case intro.intro
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure U)
w : E
hwU : w ∈ closure U
hle : IsMaxOn (norm ∘ f) (closure U) w
⊢ ∃ z, z ∈ frontier U ∧ IsMaxOn (norm ∘ f) (closure U) z
rw [closure_eq_interior_union_frontier, mem_union] at hwU
case intro.intro.inl
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure U)
w : E
hle : IsMaxOn (norm ∘ f) (closure U) w
hwU : w ∈ interior U
⊢ ∃ z, z ∈ frontier U ∧ IsMaxOn (norm ∘ f) (closure U) z

case intro.intro.inr
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure U)
w : E
hle : IsMaxOn (norm ∘ f) (closure U) w
hwU : w ∈ frontier U
⊢ ∃ z, z ∈ frontier U ∧ IsMaxOn (norm ∘ f) (closure U) z
case intro.intro
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure U)
w : E
hwU : w ∈ interior U ∨ w ∈ frontier U
hle : IsMaxOn (norm ∘ f) (closure U) w
⊢ ∃ z, z ∈ frontier U ∧ IsMaxOn (norm ∘ f) (closure U) z
cases' hwU with hwU hwU
case intro.intro.inr
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure U)
w : E
hle : IsMaxOn (norm ∘ f) (closure U) w
hwU : w ∈ frontier U
⊢ ∃ z, z ∈ frontier U ∧ IsMaxOn (norm ∘ f) (closure U) z

case intro.intro.inl
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure U)
w : E
hle : IsMaxOn (norm ∘ f) (closure U) w
hwU : w ∈ interior U
⊢ ∃ z, z ∈ frontier U ∧ IsMaxOn (norm ∘ f) (closure U) z
case intro.intro.inl
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure U)
w : E
hle : IsMaxOn (norm ∘ f) (closure U) w
hwU : w ∈ interior U
⊢ ∃ z, z ∈ frontier U ∧ IsMaxOn (norm ∘ f) (closure U) z

case intro.intro.inr
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure U)
w : E
hle : IsMaxOn (norm ∘ f) (closure U) w
hwU : w ∈ frontier U
⊢ ∃ z, z ∈ frontier U ∧ IsMaxOn (norm ∘ f) (closure U) z
rotate_left
case intro.intro.inl
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure U)
w : E
hle : IsMaxOn (norm ∘ f) (closure U) w
hwU : w ∈ interior U
this : interior U ≠ univ
⊢ ∃ z, z ∈ frontier U ∧ IsMaxOn (norm ∘ f) (closure U) z
case intro.intro.inl
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure U)
w : E
hle : IsMaxOn (norm ∘ f) (closure U) w
hwU : w ∈ interior U
⊢ ∃ z, z ∈ frontier U ∧ IsMaxOn (norm ∘ f) (closure U) z
have : interior U ≠ univ := ne_top_of_le_ne_top hc.ne_univ interior_subset_closure
case intro.intro.inl.intro.intro
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure U)
w : E
hle : IsMaxOn (norm ∘ f) (closure U) w
hwU : w ∈ interior U
this : interior U ≠ univ
z : E
hzU : z ∈ frontier (interior U)
hzw : infDist w (interior Uᶜ) = dist w z
⊢ ∃ z, z ∈ frontier U ∧ IsMaxOn (norm ∘ f) (closure U) z
case intro.intro.inl
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure U)
w : E
hle : IsMaxOn (norm ∘ f) (closure U) w
hwU : w ∈ interior U
this : interior U ≠ univ
⊢ ∃ z, z ∈ frontier U ∧ IsMaxOn (norm ∘ f) (closure U) z
rcases exists_mem_frontier_infDist_compl_eq_dist hwU this with ⟨z, hzU, hzw⟩
case intro.intro.inl.intro.intro
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure U)
w : E
hle : IsMaxOn (norm ∘ f) (closure U) w
hwU : w ∈ interior U
this : interior U ≠ univ
z : E
hzU : z ∈ frontier (interior U)
hzw : infDist w (interior Uᶜ) = dist w z
x : E
hx : x ∈ closure U
⊢ (norm ∘ f) w = (norm ∘ f) z
case intro.intro.inl.intro.intro
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure U)
w : E
hle : IsMaxOn (norm ∘ f) (closure U) w
hwU : w ∈ interior U
this : interior U ≠ univ
z : E
hzU : z ∈ frontier (interior U)
hzw : infDist w (interior Uᶜ) = dist w z
⊢ ∃ z, z ∈ frontier U ∧ IsMaxOn (norm ∘ f) (closure U) z
refine' ⟨z, frontier_interior_subset hzU, fun x hx => (hle hx).out.trans_eq _⟩
case intro.intro.inl.intro.intro
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure U)
w : E
hle : IsMaxOn (norm ∘ f) (closure U) w
hwU : w ∈ interior U
this : interior U ≠ univ
z : E
hzU : z ∈ frontier (interior U)
hzw : infDist w (interior Uᶜ) = dist w z
x : E
hx : x ∈ closure U
⊢ ball w (dist z w) ⊆ U
case intro.intro.inl.intro.intro
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure U)
w : E
hle : IsMaxOn (norm ∘ f) (closure U) w
hwU : w ∈ interior U
this : interior U ≠ univ
z : E
hzU : z ∈ frontier (interior U)
hzw : infDist w (interior Uᶜ) = dist w z
x : E
hx : x ∈ closure U
⊢ (norm ∘ f) w = (norm ∘ f) z
refine' (norm_eq_norm_of_isMaxOn_of_ball_subset hd (hle.on_subset subset_closure) _).symm
case intro.intro.inl.intro.intro
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure U)
w : E
hle : IsMaxOn (norm ∘ f) (closure U) w
hwU : w ∈ interior U
this : interior U ≠ univ
z : E
hzU : z ∈ frontier (interior U)
hzw : infDist w (interior Uᶜ) = dist w z
x : E
hx : x ∈ closure U
⊢ ball w (infDist w (interior Uᶜ)) ⊆ U
case intro.intro.inl.intro.intro
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure U)
w : E
hle : IsMaxOn (norm ∘ f) (closure U) w
hwU : w ∈ interior U
this : interior U ≠ univ
z : E
hzU : z ∈ frontier (interior U)
hzw : infDist w (interior Uᶜ) = dist w z
x : E
hx : x ∈ closure U
⊢ ball w (dist z w) ⊆ U
rw [dist_comm, ← hzw]
no goals
case intro.intro.inl.intro.intro
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure U)
w : E
hle : IsMaxOn (norm ∘ f) (closure U) w
hwU : w ∈ interior U
this : interior U ≠ univ
z : E
hzU : z ∈ frontier (interior U)
hzw : infDist w (interior Uᶜ) = dist w z
x : E
hx : x ∈ closure U
⊢ ball w (infDist w (interior Uᶜ)) ⊆ U
exact ball_infDist_compl_subset.trans interior_subset
no goals
case intro.intro.inr
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure U)
w : E
hle : IsMaxOn (norm ∘ f) (closure U) w
hwU : w ∈ frontier U
⊢ ∃ z, z ∈ frontier U ∧ IsMaxOn (norm ∘ f) (closure U) z
exact ⟨w, hwU, hle⟩