union — Mathlib

English

In a directed order, the union of bounded above sets is bounded above.

Русский

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

LaTeX

$$Theorem with directed order: BddAbove s → BddAbove t → BddAbove (s ∪ t).$$

Lean4

/-- In a directed order, the union of bounded above sets is bounded above. -/
theorem union [IsDirected α (· ≤ ·)] {s t : Set α} : BddAbove s → BddAbove t → BddAbove (s ∪ t) :=
  by
  rintro ⟨a, ha⟩ ⟨b, hb⟩
  obtain ⟨c, hca, hcb⟩ := exists_ge_ge a b
  rw [BddAbove, upperBounds_union]
  exact ⟨c, upperBounds_mono_mem hca ha, upperBounds_mono_mem hcb hb⟩

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