English
In a finite-dimensional real normed space, given x ∈ s, there exists y ∈ frontier s with infDist x to sᶜ equal to dist(x,y).
Русский
В конечномерном вещественном нормированном пространстве найдётся точка на границе s с infDist(x, sᶜ) = dist(x,y).
LaTeX
$$$\\exists y \\in frontier\\; s,\\; \\operatorname{infDist}(x, s^{c}) = \\operatorname{dist}(x,y)$$$
Lean4
/-- If `E` is a finite-dimensional normed real vector space, `x : E`, and `s` is a neighborhood of
`x` that is not equal to the whole space, then there exists a point `y ∈ frontier s` at distance
`Metric.infDist x sᶜ` from `x`. See also
`IsCompact.exists_mem_frontier_infDist_compl_eq_dist`. -/
theorem exists_mem_frontier_infDist_compl_eq_dist {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
[FiniteDimensional ℝ E] {x : E} {s : Set E} (hx : x ∈ s) (hs : s ≠ univ) :
∃ y ∈ frontier s, Metric.infDist x sᶜ = dist x y :=
by
rcases Metric.exists_mem_closure_infDist_eq_dist (nonempty_compl.2 hs) x with ⟨y, hys, hyd⟩
rw [closure_compl] at hys
refine ⟨y, ⟨Metric.closedBall_infDist_compl_subset_closure hx <| Metric.mem_closedBall.2 <| ge_of_eq ?_, hys⟩, hyd⟩
rwa [dist_comm]
