mem_cthickening_of_edist_le — Mathlib

English

If x ∈ E, then for any δ with edist x y ≤ ENNReal.ofReal δ for some y ∈ E, we have x ∈ cthickening δ E.

Русский

Если x ∈ E, тогда при любом δ с edist x y ≤ ENNReal.ofReal δ для некоторого y ∈ E имеет место x ∈ cthickening δ E.

LaTeX

$$$ y \in E \; \Rightarrow\; x \in E \wedge edist(x,y) \le ENNReal.ofReal(δ) \Rightarrow x \in cthickening δ E $$$

Lean4

theorem mem_cthickening_of_edist_le (x y : α) (δ : ℝ) (E : Set α) (h : y ∈ E) (h' : edist x y ≤ ENNReal.ofReal δ) :
    x ∈ cthickening δ E :=
  (infEdist_le_edist_of_mem h).trans h'

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