cthickening_eq_preimage_infEdist — Mathlib

English

The closed thickening is the preimage of the interval (−∞, δ] under the function infEdist(·, E).

Русский

Закрытое утолщение является предобразом интервального множества (−∞, δ] под функцией infEdist(·, E).

LaTeX

$$$ cthickening δ E = infEdist^{-1}((-\infty, δ]) $$$

Lean4

theorem cthickening_eq_preimage_infEdist (δ : ℝ) (E : Set α) :
    cthickening δ E = (fun x => infEdist x E) ⁻¹' Iic (ENNReal.ofReal δ) :=
  rfl

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