Theorems · Theorem · order theory

ciSup_exists_le

∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] {p : ι → Prop} {f : Exists p → α},
  ⨆ (ih : Exists p), f ih ≤ ⨆ i, ⨆ (h : p i), f ⋯

Note that equality need not hold: consider ι := Bool, p := (·), α := ℤ, f := fun _ ↦ -1, then the LHS is -1 but the RHS is -1 ⊔ sSup ∅ = -1 ⊔ 0 = 0.

Defined in

Mathlib.Order.ConditionallyCompleteLattice.Indexed

Cited by

2 results in Mathlib

Foundations

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

Assumes

ConditionallyCompleteLattice