English
Let α be a pseudo-EMetric space, E ⊆ α, and δ ∈ ℝ. Then x ∈ cthickening δ E if and only if the distance from x to E (in the infimum sense) is at most δ, i.e. infEdist x E ≤ ENNReal.ofReal δ.
Русский
Пусть α — псевдометрическое пространство, E ⊆ α и δ ∈ ℝ. Тогда x ∈ cthickening δ E тогда же, когда расстояние от x до E в инфимном смысле не больше δ, то есть infEdist x E ≤ ENNReal.ofReal δ.
LaTeX
$$$ x \in cthickening δ E \iff infEdist x E \le ENNReal.ofReal(δ) $$$
Lean4
@[simp]
theorem mem_cthickening_iff : x ∈ cthickening δ s ↔ infEdist x s ≤ ENNReal.ofReal δ :=
Iff.rfl