bddAbove_insert — Mathlib

English

In a directed poset, adding a single point preserves boundedness above: BddAbove(insert a s) is equivalent to BddAbove s.

Русский

В направленном частично упорядоченном множестве добавление элемента сохраняет ограниченность сверху: BddAbove(insert a s) эквивалентно BddAbove s.

LaTeX

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

Lean4

/-- Adding a point to a set preserves its boundedness above. -/
@[simp]
theorem bddAbove_insert [IsDirected α (· ≤ ·)] {s : Set α} {a : α} : BddAbove (insert a s) ↔ BddAbove s := by
  simp only [insert_eq, bddAbove_union, bddAbove_singleton, true_and]

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