mem_thickening_iff_infEdist_lt

Mathlib.Topology.MetricSpace.Thickening

URI: https://scilib.ai/kg/mathlib#Metric.mem_thickening_iff_infEdist_lt

English

For given E and x, membership x ∈ thickening δ E is equivalent to infEdist x E < δ.

Русский

Для множества E и точки x принадлежность x thickening δ E эквивалентна тому, что infEdist x E < δ.

LaTeX

$$$x\\in thickening\\,\\delta\\,E \\iff infEdist\\,x\\,E < ENNReal.ofReal\\,\\delta$$$

Lean4

theorem mem_thickening_iff_infEdist_lt : x ∈ thickening δ s ↔ infEdist x s < ENNReal.ofReal δ :=
  Iff.rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru