infDist_zero_of_mem_closure — Mathlib

English

Infimum distance is preserved under isometries: applying an isometry to x and t preserves infDist.

Русский

Инфинум расстояния сохраняется при изометрии: применение изометрии к точке x и множеству t сохраняет infDist.

LaTeX

$$infDist (\Phi x) (\Phi '' t) = infDist x t$$

Lean4

/-- If a point belongs to the closure of `s`, then its infimum distance to `s` equals zero.
The converse is true provided that `s` is nonempty, see `Metric.mem_closure_iff_infDist_zero`. -/
theorem infDist_zero_of_mem_closure (hx : x ∈ closure s) : infDist x s = 0 :=
  by
  rw [← infDist_closure]
  exact infDist_zero_of_mem hx

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