erase — Mathlib

English

The erase operation removes a from an upper set, producing the largest upper subset not containing a.

Русский

Операция erase удаляет элемент a из верхнего множества, получая наибольший верхний фрагмент без a.

LaTeX

$$$\\mathrm{erase}(s, a) = s \\setminus \\operatorname{Iic}(a)$$$

Lean4

/-- The biggest upper subset of a upper set `s` not containing an element `a`. -/
def erase (s : UpperSet α) (a : α) : UpperSet α
    where
  carrier := s \ LowerSet.Iic a
  upper' := s.upper.sdiff_of_isLowerSet (LowerSet.Iic a).lower

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