mem_cthickening_of_dist_le — Mathlib

English

If there exists y ∈ E with dist(x,y) ≤ δ, then x ∈ cthickening δ E.

Русский

Если существует y ∈ E такое, что dist(x,y) ≤ δ, то x ∈ cthickening δ E.

LaTeX

$$$ y \in E \wedge dist(x,y) \le δ\; \Rightarrow\; x \in cthickening δ E $$$

Lean4

theorem mem_cthickening_of_dist_le {α : Type*} [PseudoMetricSpace α] (x y : α) (δ : ℝ) (E : Set α) (h : y ∈ E)
    (h' : dist x y ≤ δ) : x ∈ cthickening δ E :=
  by
  apply mem_cthickening_of_edist_le x y δ E h
  rw [edist_dist]
  exact ENNReal.ofReal_le_ofReal h'

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