mem_thickening_iff_infDist_lt — Mathlib

English

In a metric space with x nonempty E, x ∈ thickening δ E iff infDist x E < δ.

Русский

В метрическом пространстве, если E непусто, тогда x ∈ thickening δ E тогда и только тогда, когда infDist x E < δ.

LaTeX

$$$x \\in thickening\\,δ\\,E \\iff infDist\\,x\\,E < δ$$$

Lean4

theorem mem_thickening_iff_infDist_lt {E : Set X} {x : X} (h : E.Nonempty) : x ∈ thickening δ E ↔ infDist x E < δ :=
  lt_ofReal_iff_toReal_lt (infEdist_ne_top h)

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