English
In a directed poset with reverse direction, boundedness below is preserved by insertion: BddBelow(insert a s) ↔ BddBelow s.
Русский
В направленном по отношению к противоложному порядку множестве ограниченность снизу сохраняется при добавлении элемента: BddBelow(insert a s) ↔ BddBelow s.
LaTeX
$$$\\operatorname{BddBelow}(\\mathrm{insert}\\ a\\ s) \\iff \\operatorname{BddBelow}(s)$$$
Lean4
/-- Adding a point to a set preserves its boundedness below. -/
@[simp]
theorem bddBelow_insert [IsDirected α (· ≥ ·)] {s : Set α} {a : α} : BddBelow (insert a s) ↔ BddBelow s := by
simp only [insert_eq, bddBelow_union, bddBelow_singleton, true_and]
