infEdist_anti

Mathlib.Topology.MetricSpace.HausdorffDistance

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

English

If s is contained in t, then the distance from x to t is at most the distance from x to s: infEdist x t ≤ infEdist x s.

Русский

Если s ⊆ t, то infEdist x t ≤ infEdist x s.

LaTeX

$$$\forall x\forall s\forall t\ (s \subseteq t \Rightarrow \infEdist x t \le \infEdist x s)$$$

Lean4

/-- The edist is antitone with respect to inclusion. -/
theorem infEdist_anti (h : s ⊆ t) : infEdist x t ≤ infEdist x s :=
  iInf_le_iInf_of_subset h

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

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

Разделы

Аффилиация

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