erase — Mathlib

English

If s is upper and every element b ∈ s with b ≤ a must equal a, then removing a single point a from s yields an upper set.

Русский

Если s — верхнее множество и для каждого b ∈ s с b ≤ a верно b = a, тогда удаление точки a из s сохраняет свойство верхности.

LaTeX

$$$IsUpperSet s \\to (\\forall b \\in s, b \\le a \\to b = a) \\to IsUpperSet(s \\setminus \\{a\\})$$$

Lean4

theorem erase (hs : IsUpperSet s) (has : ∀ b ∈ s, b ≤ a → b = a) : IsUpperSet (s \ { a }) :=
  hs.sdiff <| by simpa using has

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