mem_thickening_iff_exists_edist_lt

English

As δ → 0, the multiplicative indicators of closed δ-thickenings converge to the indicator of closure(E).

Русский

При δ → 0 предел индикаторов закрытых δ-уплотнений сходится к индикатору замыкания(E).

LaTeX

$$$\\mathrm{Tendsto}\\bigl(\\lambda δ. (\\mathrm{Metric.cthickening}_{δ} E).\\mathrm{mulIndicator} f\\bigr)\\ (\\mathcal{N}\\;0)\\ (\\mathcal{N}((\\overline{E}).\\mathrm{mulIndicator} f))$$$

Lean4

theorem mem_thickening_iff_exists_edist_lt {δ : ℝ} (E : Set α) (x : α) :
    x ∈ thickening δ E ↔ ∃ z ∈ E, edist x z < ENNReal.ofReal δ :=
  infEdist_lt_iff

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