insert — Mathlib

English

If s is bounded below, then inserting a preserves boundedness below: BddBelow(s) → BddBelow(insert a s).

Русский

Если множество ограничено снизу, то вставка элемента сохраняет ограниченность снизу.

LaTeX

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

Lean4

protected theorem insert [IsDirected α (· ≥ ·)] {s : Set α} (a : α) : BddBelow s → BddBelow (insert a s) :=
  bddBelow_insert.2

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