bddAbove_union — Mathlib

English

In a directed order, the union of two sets is bounded above iff both are bounded above.

Русский

В направленном порядке объединение двух множеств ограничено сверху тогда и только тогда, когда каждое из них ограничено сверху.

LaTeX

$$$BddAbove(s) \\land BddAbove(t) \\iff BddAbove(s \\cup t)$ under directed order.$$

Lean4

/-- In a directed order, the union of two sets is bounded above if and only if both sets are. -/
theorem bddAbove_union [IsDirected α (· ≤ ·)] {s t : Set α} : BddAbove (s ∪ t) ↔ BddAbove s ∧ BddAbove t :=
  ⟨fun h => ⟨h.mono subset_union_left, h.mono subset_union_right⟩, fun h => h.1.union h.2⟩

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