erase — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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