English
Let E be a normed real vector space. For δ>0 and any s, infEdist x (thickening δ s) = infEdist x s - ENNReal.ofReal δ.
Русский
Пусть E — нормированное вещественное векторное пространство. Для δ>0 и любого s: infEdist x (thickening δ s) = infEdist x s − ENNReal.ofReal δ.
LaTeX
$$$$\forall x\in E:\; \operatorname{infEdist}(x, \operatorname{thickening}(\delta, s)) = \operatorname{infEdist}(x, s) - \operatorname{ENNReal}.ofReal(\delta), \quad δ>0.$$$$
Lean4
@[simp]
theorem infEdist_cthickening (δ : ℝ) (s : Set E) (x : E) :
infEdist x (cthickening δ s) = infEdist x s - ENNReal.ofReal δ :=
by
obtain hδ | hδ := le_or_gt δ 0
· rw [cthickening_of_nonpos hδ, infEdist_closure, ofReal_of_nonpos hδ, tsub_zero]
· rw [← closure_thickening hδ, infEdist_closure, infEdist_thickening hδ]
