cthickening' — Mathlib

English

The c-thickening of a lower set is again a lower set.

Русский

c-утолщение нижнего множества остаётся нижним множеством.

LaTeX

$$$\text{cthickening}(\epsilon, s) \text{ is a lower set if } s \text{ is lower}$$$

Lean4

@[to_additive IsLowerSet.cthickening]
protected theorem cthickening' (hs : IsLowerSet s) (ε : ℝ) : IsLowerSet (cthickening ε s) :=
  by
  rw [cthickening_eq_iInter_thickening'']
  exact isLowerSet_iInter₂ fun δ _ => hs.thickening' _

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