thickening_eq_empty_iff — Mathlib

English

The thickening is empty precisely when ε ≤ 0 or s is empty.

Русский

Утолщение пусто тогда и только тогда, когда ε ≤ 0 или s пусто.

LaTeX

$$$\\mathrm{thickening}_{\\varepsilon}(s) = \\emptyset \\iff \\varepsilon \\le 0 \\lor s = \\emptyset$$$

Lean4

@[simp]
theorem thickening_eq_empty_iff : thickening ε s = ∅ ↔ ε ≤ 0 ∨ s = ∅ :=
  by
  obtain hε | hε := lt_or_ge 0 ε
  · simp [thickening_eq_empty_iff_of_pos, hε]
  · simp [hε, thickening_of_nonpos hε]

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