cthickening_cthickening — Mathlib

English

For any δ>0 and any set s, x ∈ thickening δ s iff there exists z ∈ s with dist(x,z) < δ.

Русский

Для любого δ>0 и множества s верно: x принадлежит thickening δ s тогда и только тогда, когда существует z ∈ s такое, что dist(x,z) < δ.

LaTeX

$$$$\forall x,s,\forall δ>0:\; x \in \operatorname{thickening}(δ,s) \iff \exists z\in s:\ operatorname{dist}(x,z) < δ. $$$$

Lean4

@[simp]
theorem cthickening_cthickening (hε : 0 ≤ ε) (hδ : 0 ≤ δ) (s : Set E) :
    cthickening ε (cthickening δ s) = cthickening (ε + δ) s :=
  (cthickening_cthickening_subset hε hδ _).antisymm fun x =>
    by
    simp_rw [mem_cthickening_iff, ENNReal.ofReal_add hε hδ, infEdist_cthickening]
    exact tsub_le_iff_right.2

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