infsep_le_of_mem_of_edist_le — Mathlib

English

If x∈s, y∈s, x≠y, and dist(x,y) ≤ d, then s.infsep ≤ d.

Русский

Если x,y ∈ s, x ≠ y, и dist(x,y) ≤ d, то s.infsep ≤ d.

LaTeX

$$$ hx:\ x \in s \rightarrow hy:\ y \in s \rightarrow hxy: x \neq y \rightarrow dist x y \le d \rightarrow s.infsep \le d $$$

Lean4

theorem infsep_le_of_mem_of_edist_le {d x} (hx : x ∈ s) {y} (hy : y ∈ s) (hxy : x ≠ y) (hxy' : dist x y ≤ d) :
    s.infsep ≤ d :=
  le_trans (infsep_le_dist_of_mem hx hy hxy) hxy'

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