mem_cthickening_iff — Mathlib

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

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