English
Let α be a preorder that is downward directed with respect to ≥. If s and t are subsets of α that are bounded below, then their union s ∪ t is also bounded below.
Русский
Пусть α упорядочено частично и пониженно направлено относительно порядка ≥. Если s и t — подмножества α, ограниченные снизу, то их объединение s ∪ t ограничено снизу.
LaTeX
$$$[IsDirected α (\cdot \ge \cdot)] {s t : Set α} \; BddBelow s \to BddBelow t \to BddBelow (s \cup t)$$$
Lean4
/-- In a codirected order, the union of bounded below sets is bounded below. -/
theorem union [IsDirected α (· ≥ ·)] {s t : Set α} : BddBelow s → BddBelow t → BddBelow (s ∪ t) :=
@BddAbove.union αᵒᵈ _ _ _ _
