thickening — Mathlib

English

For δ real and E ⊆ α, x ∈ thickening δ E if and only if infEdist x E < δ.

Русский

Для δ ∈ ℝ и E ⊆ α верно: x ∈ thickening δ E тогда и только тогда, когда infEdist x E < δ.

LaTeX

$$$x\\in thickening\\,\\delta\\,E \\iff infEdist\\,x\\,E < ENNReal.ofReal\\,\\delta$$$

Lean4

/-- The (open) `δ`-thickening `Metric.thickening δ E` of a subset `E` in a pseudo emetric space
consists of those points that are at distance less than `δ` from some point of `E`. -/
def thickening (δ : ℝ) (E : Set α) : Set α :=
  {x : α | infEdist x E < ENNReal.ofReal δ}

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