thickening' — Mathlib

English

If s is a lower set, then its thickening by ε is again a lower set for any ε.

Русский

Если s — нижнее множество, то его утолщение на ε также является нижним множеством.

LaTeX

$$$\text{If } s \text{ is a lower set, then } \text{thickening}(\epsilon, s) \text{ is a lower set}$$$

Lean4

@[to_additive IsLowerSet.thickening]
protected theorem thickening' (hs : IsLowerSet s) (ε : ℝ) : IsLowerSet (thickening ε s) :=
  by
  rw [← ball_mul_one]
  exact hs.mul_left

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