English
IsCompact K in a real normed space ensures an analogous frontier-infDist equality with a point in frontier K when x ∈ K.
Русский
Компактное множество K в вещественном нормированном пространстве обеспечивает аналогичное соотношение frontier-infDist для точки x ∈ K.
LaTeX
$$IsCompact K ⇒ ∃ y ∈ frontier K, infDist x Kᶜ = dist x y$$
Lean4
/-- If `K` is a compact set in a nontrivial real normed space and `x ∈ K`, then there exists a point
`y` of the boundary of `K` at distance `Metric.infDist x Kᶜ` from `x`. See also
`exists_mem_frontier_infDist_compl_eq_dist`. -/
nonrec theorem exists_mem_frontier_infDist_compl_eq_dist {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
[Nontrivial E] {x : E} {K : Set E} (hK : IsCompact K) (hx : x ∈ K) :
∃ y ∈ frontier K, Metric.infDist x Kᶜ = dist x y :=
by
obtain hx' | hx' : x ∈ interior K ∪ frontier K :=
by
rw [← closure_eq_interior_union_frontier]
exact subset_closure hx
· rw [mem_interior_iff_mem_nhds, Metric.nhds_basis_closedBall.mem_iff] at hx'
rcases hx' with ⟨r, hr₀, hrK⟩
have : FiniteDimensional ℝ E :=
.of_isCompact_closedBall ℝ hr₀ (hK.of_isClosed_subset Metric.isClosed_closedBall hrK)
exact exists_mem_frontier_infDist_compl_eq_dist hx hK.ne_univ
· refine ⟨x, hx', ?_⟩
rw [frontier_eq_closure_inter_closure] at hx'
rw [Metric.infDist_zero_of_mem_closure hx'.2, dist_self]
