mem_thickening_iff — Mathlib

English

The δ-thickening of a singleton {x} equals the open ball of radius δ centered at x.

Русский

δ-уплотнение множества {x} равно открытой шаре радиуса δ с центром в x.

LaTeX

$$$thickening\\,δ\\,({x}:\\ Set X) = ball\\,x\\,δ$$$

Lean4

/-- A point in a metric space belongs to the (open) `δ`-thickening of a subset `E` if and only if
it is at distance less than `δ` from some point of `E`. -/
theorem mem_thickening_iff {E : Set X} {x : X} : x ∈ thickening δ E ↔ ∃ z ∈ E, dist x z < δ :=
  by
  have key_iff : ∀ z : X, edist x z < ENNReal.ofReal δ ↔ dist x z < δ := fun z ↦ by
    rw [dist_edist, lt_ofReal_iff_toReal_lt (edist_ne_top _ _)]
  simp_rw [mem_thickening_iff_exists_edist_lt, key_iff]

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