continuous_infEdist

Mathlib.Topology.MetricSpace.HausdorffDistance

URI: https://scilib.ai/kg/mathlib#EMetric.continuous_infEdist

← MathLib Explorer

English

infEdist x s ≤ edist x y + infEdist y s.

Русский

infEdist x s ≤ edist x y + infEdist y s.

LaTeX

$$$\infEdist x s \le edist x y + \infEdist y s$$$

Lean4

/-- The edist to a set depends continuously on the point -/
@[continuity, fun_prop]
theorem continuous_infEdist : Continuous fun x => infEdist x s :=
  continuous_of_le_add_edist 1 (by simp) <| by simp only [one_mul, infEdist_le_infEdist_add_edist, forall₂_true_iff]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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