English
Let E be a normed real vector space. If ε>0 and δ>0, then thickening ε (thickening δ s) = thickening (ε+δ) s for any set s.
Русский
Пусть E — нормированное вещественное векторное пространство. Если ε>0 и δ>0, то thickening ε (thickening δ s) = thickening (ε+δ) s для любого множества s.
LaTeX
$$$$\forall s\subseteq E:\; \operatorname{thickening}(\varepsilon, \operatorname{thickening}(\delta, s)) = \operatorname{thickening}(\varepsilon+\delta, s), \quad \varepsilon>0,\ \delta>0.$$$$
Lean4
@[simp]
theorem thickening_thickening (hε : 0 < ε) (hδ : 0 < δ) (s : Set E) :
thickening ε (thickening δ s) = thickening (ε + δ) s :=
(thickening_thickening_subset _ _ _).antisymm fun x =>
by
simp_rw [mem_thickening_iff]
rintro ⟨z, hz, hxz⟩
rw [add_comm] at hxz
obtain ⟨y, hxy, hyz⟩ := exists_dist_lt_lt hε hδ hxz
exact ⟨y, ⟨_, hz, hyz⟩, hxy⟩
