insert — Mathlib

English

If s is bounded above, then inserting a does not destroy boundedness above: BddAbove s implies BddAbove(insert a s).

Русский

Если множество ограничено сверху, то вставка элемента не разрушает верхнюю границу: BddAbove s → BddAbove(insert a s).

LaTeX

$$$\\operatorname{BddAbove}(s) \\rightarrow \\operatorname{BddAbove}(\\mathrm{insert}\\ a\\ s)$$$

Lean4

protected theorem insert [IsDirected α (· ≤ ·)] {s : Set α} (a : α) : BddAbove s → BddAbove (insert a s) :=
  bddAbove_insert.2

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