thickening_eq_preimage_infEdist — Mathlib

English

The open thickening equals the preimage of the open interval under infEdist: thickening δ E = {x : infEdist x E < δ}.

Русский

Открытое уплотнение равно предобразному образу открытого интервала под infEdist: thickening δ E = {x : infEdist x E < δ}.

LaTeX

$$$thickening\\,δ\\,E = (infEdist\\,·\\,E)^{-1}(Iio(ENNReal.ofReal\\,δ))$$$

Lean4

/-- The (open) thickening equals the preimage of an open interval under `EMetric.infEdist`. -/
theorem thickening_eq_preimage_infEdist (δ : ℝ) (E : Set α) :
    thickening δ E = (infEdist · E) ⁻¹' Iio (ENNReal.ofReal δ) :=
  rfl

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