infDist_inter_closedBall_of_mem — Mathlib

English

If y ∈ s, then infDist x (s ∩ closedBall x (dist y x)) = infDist x s.

Русский

Если y ∈ s, тогда infDist x (s ∩ замкнутый шар) = infDist x s.

LaTeX

$$infDist x (s \cap \overline{B}(x, \operatorname{dist}(y,x))) = infDist x s$$

Lean4

theorem infDist_inter_closedBall_of_mem (h : y ∈ s) : infDist x (s ∩ closedBall x (dist y x)) = infDist x s :=
  by
  replace h : y ∈ s ∩ closedBall x (dist y x) := ⟨h, mem_closedBall.2 le_rfl⟩
  refine le_antisymm ?_ (infDist_le_infDist_of_subset inter_subset_left ⟨y, h⟩)
  refine not_lt.1 fun hlt => ?_
  rcases (infDist_lt_iff ⟨y, h.1⟩).mp hlt with ⟨z, hzs, hz⟩
  rcases le_or_gt (dist z x) (dist y x) with hle | hlt
  · exact hz.not_ge (infDist_le_dist_of_mem ⟨hzs, hle⟩)
  · rw [dist_comm z, dist_comm y] at hlt
    exact (hlt.trans hz).not_ge (infDist_le_dist_of_mem h)

Похожие утверждения