infDist_le_infDist_of_subset — Mathlib

English

If s is contained in t and s is nonempty, then the minimal distance to t from x is at most the minimal distance to s from x.

Русский

Если s ⊆ t и s непусто, то infDist(x, t) ≤ infDist(x, s).

LaTeX

$$$(s \subseteq t) \land (s \neq \varnothing) \Rightarrow \infDist x t \le \infDist x s$$$

Lean4

/-- The minimal distance is monotone with respect to inclusion. -/
theorem infDist_le_infDist_of_subset (h : s ⊆ t) (hs : s.Nonempty) : infDist x t ≤ infDist x s :=
  ENNReal.toReal_mono (infEdist_ne_top hs) (infEdist_anti h)

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