Theorems · Theorem · order theory

BddBelow.union

∀ {α : Type u_1} [inst : Preorder α] [IsCodirectedOrder α] {s t : Set α}, BddBelow s → BddBelow t → BddBelow (s ∪ t)

In a codirected order, the union of bounded below sets is bounded below.

Defined in

Mathlib.Order.Bounds.Basic

Cited by

1 results in Mathlib

Foundations

Depth 8 from the axioms · uses propext, Quot.sound

Assumes

PreorderIsCodirectedOrder