English
For a closed nonempty set s in a proper space, for any x there exists y ∈ s with infDist x s = dist x y.
Русский
Для замкнутого непустого множества s в пространстве proper существует y ∈ s такое, что infDist x s = dist x y.
LaTeX
$$IsClosed s → s.Nonempty → ∀ x, ∃ y ∈ s, infDist x s = dist x y$$
Lean4
theorem _root_.IsClosed.exists_infDist_eq_dist [ProperSpace α] (h : IsClosed s) (hne : s.Nonempty) (x : α) :
∃ y ∈ s, infDist x s = dist x y := by
rcases hne with ⟨z, hz⟩
rw [← infDist_inter_closedBall_of_mem hz]
set t := s ∩ closedBall x (dist z x)
have htc : IsCompact t := (isCompact_closedBall x (dist z x)).inter_left h
have htne : t.Nonempty := ⟨z, hz, mem_closedBall.2 le_rfl⟩
obtain ⟨y, ⟨hys, -⟩, hyd⟩ : ∃ y ∈ t, infDist x t = dist x y := htc.exists_infDist_eq_dist htne x
exact ⟨y, hys, hyd⟩
