Theorems · Theorem · order theory

biSup_sup

∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {p : ι → Prop} {f : (i : ι) → p i → α} {a : α},
  (∃ i, p i) → (⨆ i, ⨆ (h : p i), f i h) ⊔ a = ⨆ i, ⨆ (h : p i), f i h ⊔ a

Defined in

Mathlib.Order.CompleteLattice.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CompleteLattice