Theorems · Theorem · order theory

Set.Finite.bddAbove_biUnion

∀ {α : Type u} {β : Type v} [inst : Preorder α] [IsDirectedOrder α] [Nonempty α] {I : Set β} {S : β → Set α},
  I.Finite → (BddAbove (⋃ i ∈ I, S i) ↔ ∀ i ∈ I, BddAbove (S i))

A finite union of sets which are all bounded above is still bounded above.

Defined in

Mathlib.Data.Set.Finite.Lattice

Cited by

0 results in Mathlib

Foundations

Depth 68 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PreorderIsDirectedOrderNonempty