cthickening — Mathlib

English

The frontier of thickening δ E is contained in the level set {x | infEdist x E = ENNReal.ofReal δ}.

Русский

Граница thickening δ E содержится в множества Q = {x | infEdist x E = ENNReal.ofReal δ}.

LaTeX

$$$\\text{frontier}(\\mathrm{thickening}\\,δ\\,E) \\subseteq \\{x : infEdist x E = ENNReal.ofReal δ\\}$$$

Lean4

/-- The closed `δ`-thickening `Metric.cthickening δ E` of a subset `E` in a pseudo emetric space
consists of those points that are at infimum distance at most `δ` from `E`. -/
def cthickening (δ : ℝ) (E : Set α) : Set α :=
  {x : α | infEdist x E ≤ ENNReal.ofReal δ}

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