thickening_cthickening — Mathlib

English

Let ε ≥ 0 and δ ≥ 0. Then thickening ε (cthickening δ s) = cthickening (ε+δ) s.

Русский

Пусть ε ≥ 0 и δ ≥ 0. Тогда thickening ε (cthickening δ s) = cthickening (ε+δ) s.

LaTeX

$$$$\forall s\subseteq E:\; \operatorname{thickening}(\varepsilon, \operatorname{cthickening}(\delta, s)) = \operatorname{cthickening}(\varepsilon+\delta, s), \quad ε \ge 0,\ δ \ge 0.$$$$

Lean4

@[simp]
theorem thickening_cthickening (hε : 0 < ε) (hδ : 0 ≤ δ) (s : Set E) :
    thickening ε (cthickening δ s) = thickening (ε + δ) s :=
  by
  obtain rfl | hδ := hδ.eq_or_lt
  · rw [cthickening_zero, thickening_closure, add_zero]
  · rw [← closure_thickening hδ, thickening_closure, thickening_thickening hε hδ]

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