infEdist_ne_top — Mathlib

English

If s is nonempty, then infEdist x s is finite (not ∞).

Русский

Если s непусто, то infEdist x s конечно, не равно ∞.

LaTeX

$$$ s \neq \varnothing \Rightarrow \operatorname{infEdist}(x,s) \neq \infty $$$

Lean4

/-- In a metric space, the minimal edistance to a nonempty set is finite. -/
theorem infEdist_ne_top (h : s.Nonempty) : infEdist x s ≠ ⊤ :=
  by
  rcases h with ⟨y, hy⟩
  exact ne_top_of_le_ne_top (edist_ne_top _ _) (infEdist_le_edist_of_mem hy)

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