le_edist_of_le_infsep — Mathlib

English

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

Русский

Пусть x,y ∈ s, x ≠ y, и d ≤ s.infsep; тогда d ≤ dist x y.

LaTeX

$$$ (hx: x \in s) (hy: y \in s) (hxy: x \neq y) (hd: d \le s.infsep) \Rightarrow d \le dist x y $$$

Lean4

theorem le_edist_of_le_infsep {d x} (hx : x ∈ s) {y} (hy : y ∈ s) (hxy : x ≠ y) (hd : d ≤ s.infsep) : d ≤ dist x y :=
  by
  by_cases hs : s.Nontrivial
  · exact hs.le_infsep_iff.1 hd x hx y hy hxy
  · rw [not_nontrivial_iff] at hs
    rw [hs.infsep_zero] at hd
    exact le_trans hd dist_nonneg

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