Theorems · Theorem · order theory

bddBelow_union

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

In a codirected order, the union of two sets is bounded below if and only if both sets are.

Defined in

Mathlib.Order.Bounds.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

PreorderIsCodirectedOrder